Axiom ใช้ฝูง AI agent formalize การจำแนกกรุปเชิงเดียวจำกัด (CFSG) ลง Lean ครบใน 24 วัน — 43.1 ล้านบรรทัด ไม่มี sorry และระหว่างทางเจอจุดผิดในบทพิสูจน์ที่ตีพิมพ์ตั้งแต่ปี 1986

สตาร์ทอัป Axiom Math ประกาศเมื่อ 26 ต.ค. 2026 ว่าทำ formalization ของ Classification of Finite Simple Groups (CFSG) ลง Lean 4 ได้ครบ และเปิดรีโป AxiomMath/CFSG ภายใต้ Apache-2.0 เมื่อ 27 ต.ค. CFSG คือทฤษฎีบทที่บอกว่ากรุปเชิงเดียวจำกัดทุกตัวต้องเป็นกรุปวัฏจักรอันดับเฉพาะ กรุปสลับ กรุปแบบ Lie หรือหนึ่งใน 26 กรุป sporadic บทพิสูจน์รุ่นแรกยาวหลายพันหน้าในวารสาร เขียนโดยนักคณิตศาสตร์ราวร้อยคนตลอดหลายทศวรรษ และไม่เคยมีใครคนเดียวตรวจได้ทั้งหมด

งานนี้ใช้เวลา 24 วัน โดยวิศวกรและนักคณิตศาสตร์ของ Axiom กำกับ ฝูง AI agent หลายสิบตัว ผลลัพธ์คือโค้ด Lean ประมาณ 43.1 ล้านบรรทัด และ 2.05 ล้าน declaration ตามหน้า proof map ทุกขั้นตอนตรรกะผ่านการตรวจของ kernel ของ Lean ถ้าเทียบกับ formalization ของทฤษฎีบท Feit–Thompson ใน Coq เมื่อปี 2012 ซึ่งเป็นแค่ส่วนหนึ่งของ CFSG ทีมของ Georges Gonthier ใช้เวลาถึง 6 ปี

ตรวจแล้วว่า “ครบจริง” แค่ไหน

ประเด็นที่ต้องถามทุกครั้งกับงานแบบนี้คือ statement ถูกไหม และมีช่องโหว่ซ่อนอยู่หรือเปล่า งานรอบก่อนเคยมีกรณีที่ทฤษฎีบทคลาสสิกข้างในถูกพิสูจน์แค่ “เท่าที่จำเป็น” สำหรับงานนี้ README ของรีโประบุว่า

• ไม่มี sorry บน Lean v4.35.0-rc3 สร้างบน Mathlib และ TauCeti
• ใช้แค่ axiom มาตรฐาน 3 ตัว คือ Classical.choice, propext, Quot.sound และ ไม่ใช้ native_decide ซึ่งเป็นทางลัดที่ข้ามการตรวจของ kernel
• statement ของ CFSG ไม่ได้เขียนเอง แต่ใช้ ClassificationStatement จากโปรเจกต์ TauCeti ภายนอก ความเสี่ยงที่ agent จะ “พิสูจน์สิ่งที่ง่ายกว่าโจทย์จริง” จึงลดลงมาก
• ตามบล็อกยังรวมโค้ดราว 1.2 ล้านบรรทัดจากโปรเจกต์ Qiuzhen-CFSG ด้วย

ข้อจำกัดที่ควรรู้คือ lake build ทั้งโปรเจกต์ใช้เวลา เกือบ 24 ชั่วโมง และต้องใช้การแก้ Lake ที่ยังไม่ได้ merge เข้า upstream การตรวจซ้ำโดยอิสระจึงทำได้ แต่ต้องลงทุนเครื่องพอสมควร และบทความไม่ได้เปิดเผยว่าใช้โมเดลอะไรหรือใช้ compute เท่าไร เขียนไว้แค่ว่าใช้ “ส่วนผสมของโมเดลที่เปลี่ยนไปเรื่อย ๆ” ผ่าน agent ของ AxiomProver

เจอจุดผิดในวรรณกรรมที่ตีพิมพ์แล้ว

ระหว่าง formalize ทีมพบ 34 จุดที่เบี่ยงจากเอกสารที่ตีพิมพ์ จุดใหญ่ที่สุดอยู่ในบทพิสูจน์ Unbalanced Group Theorem ของ Walter ปี 1986 ซึ่งอาศัยข้ออ้างเรื่อง closure ข้อหนึ่ง agent หา counterexample ได้ตรง ๆ คือ PSL₂(49) ที่ centralizer ของ field involution มี simple component เป็น PSL₂(7) ซึ่งเป็นกรุปที่ถูกตัดออกจากตระกูลนั้นเพราะ 7 เป็นจำนวนเฉพาะเมอร์แซนน์

ข้อผิดนี้ ไม่ได้ทำให้ทฤษฎีบทล้ม บล็อกระบุว่าเป้าหมายของ UGT ยังเป็นจริง แต่ต้องใช้เส้นทางใหม่ ทีมพิสูจน์โดยอิงทฤษฎี maximal 2-component ของ Solomon ปี 1976 และได้ผลใหม่ชื่อ “Preservation of simple tops” (Theorem 2.3) ซึ่งเขียนเป็นเปเปอร์ 35 หน้าบน Hexagon (2610.00575) ส่วน errata ทั้งหมดกำลังรวบรวมร่วมกับนักทฤษฎีกรุปและจะเผยแพร่ภายหลัง ที่ปรึกษาภายนอกมี Richard Lyons, Dan Nakano และ Ron Solomon โดย Lyons และ Solomon เป็นผู้เขียนร่วมในชุดหนังสือบทพิสูจน์รุ่นที่สองของ CFSG

วิธีทำงานของฝูง agent

ช่อง Slack ของโปรเจกต์เปิดเมื่อ 1 ต.ค. ฝูง agent ชุดแรกเริ่มทำงาน 2 ต.ค. และมีการวางแผนใหม่ครั้งใหญ่ในวันที่ 13 ต.ค. งานถูกแบ่งเป็น 108 milestone และงานย่อยราว 380 งาน อิงเอกสารต้นทาง 139 ชิ้นตั้งแต่ปี 1870 ถึง 2026 agent ระดับหัวหน้าทำหน้าที่รีวิว statement ส่วนนักคณิตศาสตร์มนุษย์ตามสืบเฉพาะจุดที่ agent ติดเพราะคณิตศาสตร์ต้นทางมีปัญหา หน้า cfsg.axiommath.ai มี proof map ให้ดูว่าแต่ละ milestone อิงเปเปอร์ไหนและผ่านการตรวจเมื่อไร

มุมมอง AI Curator

เทียบกับ การ formalize ทฤษฎีบทแฟร์มาต์ของ Claude เมื่อต้นเดือนกันยายน ที่ได้ 13 ล้านบรรทัดใน 11 วัน งานนี้ใหญ่กว่า 3 เท่าภายในเวลาไม่ถึงสองเท่า และที่สำคัญกว่าขนาดคือ ความโปร่งใสดีกว่า ไม่มี sorry, ไม่ใช้ native_decide และใช้ statement จากคนนอก สามข้อนี้คือสิ่งที่ชุมชน Lean ถามหาจากงานรอบก่อน ๆ จุดอ่อนที่ยังเหลือคือไม่บอกว่าใช้โมเดลไหนและใช้ compute เท่าไร เลยประเมินยากว่าคนอื่นจะทำซ้ำได้ด้วยงบเท่าไร

ผลที่น่าสนใจที่สุดไม่ใช่ตัวเลข 43 ล้านบรรทัด แต่เป็น 34 จุดผิดในวรรณกรรม CFSG ถูกอ้างว่า “ถูกต้อง” มาหลายสิบปีบนพื้นฐานความเชื่อใจในชุมชน งานนี้แสดงว่า AI agent ไม่ได้แค่แปลคณิตศาสตร์ที่มนุษย์เขียนไว้แล้ว แต่ยังเป็นเครื่องมือตรวจสอบเอกสารเก่าในระดับที่มนุษย์ทำไม่ไหวด้วย สำหรับนักพัฒนา บทเรียนที่ใช้ได้เลยคือรูปแบบงาน ได้แก่ statement ที่ล็อกจากภายนอก, kernel เป็นผู้ตัดสิน, milestone ที่ตรวจได้, และมนุษย์ลงมือเฉพาะจุดที่ระบบติด สูตรนี้ใช้ได้กับงาน agent ขนาดใหญ่ที่มี “ตัวตรวจ” ชัดเจน เช่น migration โค้ดที่มี test suite ครอบ สำหรับนักคณิตศาสตร์และนักศึกษาไทย รีโปที่เปิดเป็น Apache-2.0 และ proof map แบบ interactive เป็นแหล่งเรียนทฤษฎีกรุปที่ไม่เคยมีมาก่อน เพราะคลิกไล่จากทฤษฎีบทลงไปถึงเปเปอร์ต้นทางได้ทุกขั้น

แหล่งข่าว

• Axiom Math — The Enormous Theorem, Formalized (26 ต.ค. 2026)
• CFSG in Lean — proof map แบบ interactive และสถิติ
• GitHub — AxiomMath/CFSG (README: sorry-free, axioms, build time)
• Hexagon 2610.00575 — The Unbalanced Group Theorem