Axiom Math เผยแพร่บทพิสูจน์การจำแนกกรุปใน Lean ความยาว 43.1 ล้านบรรทัด

Axiom Math ระบุเมื่อวันที่ 27 ตุลาคม 2026 ว่าบริษัทกำลังเผยแพร่สิ่งที่เรียกว่าเป็นบทพิสูจน์การจำแนกกรุปอย่างง่ายจำกัด (Classification of Finite Simple Groups) ฉบับสมบูรณ์ฉบับแรกที่ผ่านการตรวจสอบด้วยคอมพิวเตอร์ บทพิสูจน์นี้จัดทำขึ้นภายใน 24 วัน โดยวิศวกรและนักคณิตศาสตร์ควบคุมฝูงเอเจนต์ AI หลายสิบตัว ซึ่งเขียนโค้ดในตัวช่วยพิสูจน์ Lean ประมาณ 43.1 ล้านบรรทัด

บริษัทเขียนไว้ในประกาศว่า “วันนี้ เรากำลังเผยแพร่บทพิสูจน์การจำแนกกรุปอย่างง่ายจำกัด (CFSG) ฉบับสมบูรณ์ฉบับแรกที่ผ่านการตรวจสอบด้วยคอมพิวเตอร์” การจำแนกนี้ระบุองค์ประกอบพื้นฐานของกรุปจำกัด ส่วนบทพิสูจน์ฉบับดั้งเดิมมีความยาวรวมประมาณ 15,000 หน้า ในบทความมากกว่า 500 ชิ้น โดยนักคณิตศาสตร์ราว 100 คน จนมีขนาดใหญ่ถึงขั้นได้รับฉายาว่าทฤษฎีบทมหึมา

สิ่งที่ Axiom เผยแพร่

CFSG ระบุว่ากรุปอย่างง่ายจำกัดทุกกรุปเป็นกรุปวัฏจักรที่มีอันดับเป็นจำนวนเฉพาะ เป็นกรุปสลับบนสัญลักษณ์อย่างน้อยห้าตัว เป็นหนึ่งใน 16 ตระกูลอนันต์ของกรุปประเภทลีที่สร้างขึ้นเหนือฟิลด์จำกัด หรือเป็นหนึ่งในกรุปสปอราดิกแบบโดดเดี่ยวจำนวน 26 กรุปพอดี โดยประกาศระบุว่าผู้เขียนบางคนจัดกรุปทิตส์เป็นกรุปที่ 27 ด้วย กรูปสปอราดิกที่ใหญ่ที่สุดคือกรุปมอนสเตอร์ ซึ่ง Robert Griess สร้างขึ้นในปี 1980 โดยใช้อัลจีบราในมิติ 196,884

ความพยายามพิสูจน์ของมนุษย์กินเวลายาวนานหลายทศวรรษ ในปี 1963 Walter Feit และ John Thompson พิสูจน์ว่ากรุปอย่างง่ายจำกัดที่ไม่เป็นอาเบเลียนทุกกรุปมีอันดับเป็นจำนวนคู่ โดยนำเสนอในบทความความยาว 255 หน้า ซึ่งตีพิมพ์เต็มวารสาร Pacific Journal of Mathematics หนึ่งฉบับ Daniel Gorenstein วางแผนงาน 16 ขั้นตอนเพื่อทำการจำแนกให้เสร็จสมบูรณ์ในปี 1972 และประกาศว่าการจำแนกเสร็จสมบูรณ์แล้วในปี 1983 แต่กรณีควาซิทินยังอาศัยต้นฉบับที่ Geoffrey Mason เขียนไว้แต่ยังไม่เสร็จ จนกระทั่ง Michael Aschbacher และ Stephen Smith ตีพิมพ์งานศึกษาความยาว 1,221 หน้าในปี 2004 จึงปิดงานที่ต่อมาเป็นที่รู้จักในชื่อบทพิสูจน์รุ่นแรก ส่วนบทพิสูจน์รุ่นที่สองซึ่งเป็นระบบมากขึ้น เริ่มต้นโดย Gorenstein และ Richard Lyons ก่อนที่ Ronald Solomon และ Inna Capdeboscq จะเข้าร่วม ยังคงไม่เสร็จสมบูรณ์ ดังนั้น Axiom จึงทำบทพิสูจน์รุ่นแรกให้อยู่ในรูปแบบทางการ

หน้าโครงการอธิบายว่าการทำให้เป็นรูปแบบทางการนี้ดำเนินตามบทพิสูจน์รุ่นแรก โดยทุกขั้นตอนทางตรรกะได้รับการตรวจสอบด้วยเคอร์เนลของ Lean และระบุว่ามีโค้ด Lean 43.1 ล้านบรรทัด นิยาม 2.05 ล้านรายการ และเอกสาร 715 ชิ้น ทั้งบทความและหนังสือ อยู่ในคลังข้อมูล Axiom ระบุว่าแผนผังบทพิสูจน์อ้างอิงจากหนังสือชุดบทพิสูจน์รุ่นที่สอง และการทำให้เป็นรูปแบบทางการนี้รวมโค้ดจากโครงการ Qiuzhen-CFSG ก่อนหน้าประมาณ 1.2 ล้านบรรทัด พร้อมต่อยอดจาก Mathlib ซึ่งบริษัทระบุว่าเกิดจากผลงานของผู้ร่วมให้ข้อมูลหลายร้อยคน โครงการระบุชื่อ Dean Cureton, Vasily Ilin, Bhavik Mehta และ Niels Voss เป็นผู้ร่วมพัฒนาหลัก โดยมี Letong Hong เป็นหัวหน้าผู้วิจัย

คลัง GitHub สาธารณะอธิบายผลงานนี้ว่าเป็นบทพิสูจน์ Lean4 ที่ไม่มีการใช้ sorry โดยตรึงไว้ที่เวอร์ชัน 4.35.0-rc3 สร้างต่อยอดจาก Mathlib และโครงการ TauCeti และใช้สัจพจน์มาตรฐานเพียง Classical.choice, propext และ Quot.sound โดยไม่ใช้ native_decide ข้อความระบุทฤษฎีบทการจำแนกอย่างเป็นทางการ ซึ่งนำมาจาก TauCeti ระบุว่า “กรุปอย่างง่ายจำกัดทุกกรุปสมสัณฐานกับกรุปหนึ่งในรายการจำแนกที่สร้างขึ้นไว้อย่างชัดเจน” ไฟล์ README ระบุว่า lake build ใช้ตรวจสอบการพัฒนาทั้งหมด และการปรับแก้เครื่องมือสร้าง Lake ที่เปิดให้ใช้งาน รวมถึงการปรับประสิทธิภาพที่ทีมวางแผนจะส่งกลับไปยังโครงการต้นทาง ช่วยลดเวลาสร้างให้ต่ำกว่า 24 ชั่วโมง โค้ดนี้เผยแพร่ภายใต้สัญญาอนุญาต Apache-2.0

ความพยายามร่วมกันของฝูงเอเจนต์ใน 24 วัน

เมื่อวันที่ 1 ตุลาคม 2026 Axiom เปิดช่อง Slack เพื่อประสานงานโครงการ งาน Lean ที่มีอยู่ก่อนแล้วและแผนผังบทพิสูจน์ภายในซึ่งรวบรวมจากเอกสารที่ตีพิมพ์ แบ่งงานออกเป็นหมุดหมาย 108 รายการและงานย่อยประมาณ 380 งาน ฝูงเอเจนต์ชุดแรกเริ่มทำงานเมื่อวันที่ 2 ตุลาคม 2026 โดยเอเจนต์รับหมุดหมายผ่านประเด็นใน GitHub และรายงานงานที่เสร็จแล้วใน Slack เอเจนต์หัวหน้าจะแยกข้อโต้แย้งที่ยากออกเป็นส่วนย่อยและทบทวนข้อความทางคณิตศาสตร์ ขณะที่เอเจนต์อื่นค้นหาผลลัพธ์ที่มีอยู่แล้วหรือเขียนบทพิสูจน์ใน Lean และเอเจนต์หนึ่งสามารถมอบหมายให้เอเจนต์อื่นจัดการเงื่อนไขพื้นฐานที่ยังขาด โดยนำผลลัพธ์ของงานเหล่านั้นเข้าไว้ในคลังข้อมูลที่ใช้ร่วมกัน

ความคืบหน้าในช่วงแรกเผยให้เห็นจุดอ่อน หมุดหมายบางรายการที่ดูเหมือนจัดการได้ไม่ยากกลับซ่อนเงื่อนไขพื้นฐานจำนวนมหาศาล ซึ่งเอเจนต์ตั้งสมมติฐานไว้แทนที่จะพิสูจน์ให้ได้ และทีมต้องลบโค้ดหลายหมื่นบรรทัดที่ตั้งอยู่บนสมมติฐานเหล่านั้น ก่อนเริ่มใหม่ด้วยแผนที่รัดกุมกว่า หมุดหมายช่วงแรกงานหนึ่งเกี่ยวข้องกับทฤษฎีบทฟังก์เตอร์ซิกนัลไลเซอร์ โดยบทพิสูจน์ที่เสนออาศัยสมมติฐานเชิงโครงสร้างซึ่งยังต้องมีการพิสูจน์รองรับ นอกจากนี้ เวลาในการสร้างยังกลายเป็นคอขวด เมื่อเอเจนต์ผลิตบทพิสูจน์ได้เร็วกว่าที่ Lean จะตรวจสอบซ้ำ Axiom ระบุว่าวิศวกรของบริษัทกระจายผลการสร้างที่แคชไว้ไปยังเครื่องประมวลผลหลายเครื่อง รันการตรวจสอบอิสระควบคู่กัน และแยกการคำนวณจำกัดที่ใช้ทรัพยากรสูงออกมาเป็นใบรับรองที่ตรวจสอบแยกได้ บริษัทระบุว่าการเปลี่ยนแปลงเหล่านี้เร่งการตรวจสอบได้หลายลำดับขนาด

บริษัทเล่าว่า เมื่อวันที่ 10 ตุลาคม 2026 มีข้อความในช่องทางประกาศว่าเอเจนต์พิสูจน์ได้แล้วว่ากรุปมอนสเตอร์เป็นกรุปอย่างง่าย นอกจากนี้ เอเจนต์ยังทำให้การมีอยู่ของกรุปมอนสเตอร์เป็นรูปแบบทางการผ่านอัลจีบรา Griess และทฤษฎีบทที่ระบุว่ากรุปประเภทมอนสเตอร์คือกรุปมอนสเตอร์ เมื่อวันที่ 13 ตุลาคม 2026 มีหมุดหมายเสร็จสิ้นเพียงรายการเดียว วิศวกรจึงจัดการวางแผนใหม่ โดยแบ่งหมุดหมายที่ยังไม่เสร็จออกเป็นทฤษฎีบทที่เล็กลงและระบุข้อความไว้อย่างแม่นยำ แต่ละการแยกย่อยต้องแสดงให้เห็นว่าทฤษฎีบทแต่ละส่วนจะใช้พิสูจน์หมุดหมายเดิมได้อย่างไร ผ่านบทพิสูจน์ Lean ที่กระชับ

พบช่องโหว่ในบทพิสูจน์ที่ตีพิมพ์แล้ว

Axiom รายงานว่า การแปลงบทพิสูจน์เป็น Lean เผยให้เห็นปัญหาในข้อโต้แย้งที่ตีพิมพ์เผยแพร่ไปแล้ว ส่วนใหญ่เป็นข้อผิดพลาดเล็กน้อย เช่น การพิมพ์ผิด ข้อผิดพลาดในตาราง หรือการตกหล่นของสมมติฐาน แต่บริษัทระบุว่าพบความคลาดเคลื่อนจากเอกสารที่เผยแพร่แล้วซึ่งควรกล่าวถึง 34 จุด โดยจุดที่สำคัญที่สุดเกี่ยวข้องกับทฤษฎีบทกรุปไม่สมดุล (Unbalanced Group Theorem หรือ UGT)

ตัวอย่างหนึ่งมาจากหนังสือว่าด้วยกรุปควาซิธินของ Aschbacher และ Smith ซึ่งมีบทตั้งที่ระบุว่าปริมาณเชิงตัวเลขสองค่ามีค่าเท่ากัน เอเจนต์พบตัวอย่างโต้แย้งที่เกี่ยวข้องกับกรุป SL₂(5) ซึ่งปริมาณหนึ่งมีค่าเป็น 1 ทั้งที่ความเท่ากันตามที่ระบุไว้กำหนดให้ค่านั้นต้องเป็น 2 การเปลี่ยนความเท่ากันเป็นอสมการช่วยแก้บทตั้งได้ แต่ข้อโต้แย้งในส่วนถัดมาอาศัยความเท่ากันดังกล่าวเพื่อตัดกรณีต่าง ๆ ออก ทีมจึงขยายข้อโต้แย้งก่อนหน้านี้ให้ครอบคลุมกรณีเหล่านั้นด้วย

UGT ช่วยระบุกรุปทั้งกรุปได้จากข้อมูลเกี่ยวกับกรุปย่อยของมัน โดยบทคัดย่อของบทความประกอบระบุว่า ภายใต้สมมติฐานอุปนัยของการจำแนกประเภท หากกรุปย่อยที่ไม่เป็นเอกลักษณ์และมีอันดับคี่เป็นกรุปปกติในตัวรวมศูนย์ของอินโวลูชัน ก็จะบังคับให้กรุปเชิงเดี่ยวโดยรอบเป็นกรุปแบบลีในลักษณะเฉพาะคี่ หรือเป็นกรุปสลับที่มีดีกรีบางค่า Axiom เริ่มศึกษาทฤษฎีบท UGT จากบันทึกความทรงจำของ John Walter ในปี 1986 และระหว่างที่ทำให้ข้อโต้แย้งดังกล่าวเป็นทางการ เอเจนต์ของบริษัทพบตัวอย่างโต้แย้งอย่างชัดเจนต่อข้อความเกี่ยวกับการปิดภายใต้การดำเนินการที่ข้อโต้แย้งนั้นใช้ กล่าวคือ การดำเนินการที่เชื่อกันว่าจะทำให้กรุปเชิงเดี่ยวที่เกี่ยวข้องยังคงอยู่ในวงศ์ที่กำหนด กลับอาจให้ผลเป็นกรุปที่ถูกยกเว้นจากวงศ์นั้นอย่างชัดเจน

ตามคำอธิบายของบริษัท เมื่อเริ่มจาก PSL₂(49) ซึ่งอินโวลูชันของฟิลด์มีตัวรวมศูนย์เป็น PGL₂(7) การดำเนินการนี้จะให้คอมโพเนนต์เชิงเดี่ยว PSL₂(7) ซึ่งถูกยกเว้นจากวงศ์ดังกล่าว เพราะ 7 เป็นจำนวนเฉพาะเมอร์แซนน์ Axiom ระบุว่าตัวอย่างโต้แย้งเหล่านี้ไม่ได้หักล้าง UGT หรือแม้แต่ข้อสรุปของข้อเสนอ II.5.9(ii) ของ Walter

การแก้ไขนี้อาศัยทฤษฎีว่าด้วย 2-component สูงสุดของ Solomon ในปี 1976 ซึ่ง Axiom ระบุว่าเป็นที่มาของแนวคิดหลักสำหรับข้อโต้แย้งทางเลือกที่ระบบ AxiomProver สร้างขึ้นและทำให้เป็นทางการ ขั้นตอนสำคัญซึ่งระบุไว้ในบทความในชื่อทฤษฎีบท 2.3 (การคงสภาพของยอดเชิงเดี่ยว) เป็นผลลัพธ์ใหม่ในทฤษฎีกรุปที่ Axiom ระบุว่า AxiomProver เป็นผู้พิสูจน์ เมื่อใช้ร่วมกับการลดรูปของ Gilman และ Solomon และทฤษฎีบทการจำแนกของ Foote และ Harris ขั้นตอนนี้จึงให้รูปแบบกรุปเชิงเดี่ยวของ UGT ซึ่งจำเป็นต่อการจำแนกประเภท หลังจากทำให้เป็นทางการแล้ว นักคณิตศาสตร์ของ Axiom พบวิธีอนุมานที่สั้นกว่าโดยใช้วิธีการรุ่นแรก ซึ่งบันทึกไว้เป็นหมายเหตุ 9.5 และได้ข้อสรุปเดียวกันโดยไม่ต้องใช้ทฤษฎีบท 2.3

บทความดังกล่าวมีชื่อว่า The Unbalanced Group Theorem เขียนโดย Colin Defant และ Ken Ono และเผยแพร่บนเซิร์ฟเวอร์บทความก่อนตีพิมพ์ Hexagon เป็นเวอร์ชัน 1 เมื่อวันที่ 27 ตุลาคม 2026 ภายใต้สัญญาอนุญาต CC BY 4.0 โดยหน้าโครงการระบุว่าบทความมีความยาว 35 หน้า Axiom ระบุว่ากำลังร่วมมือกับนักทฤษฎีกรุปเพื่อรวบรวมข้อผิดพลาดที่พบในเอกสารต่าง ๆ และจะเผยแพร่ข้อผิดพลาดเหล่านั้นบนหน้ารวมข้อผิดพลาดของโครงการ Lyons และ Solomon ซึ่งผลงานเป็นรากฐานของการจำแนกประเภท ได้ให้คำปรึกษาเกี่ยวกับการแก้ไข UGT และบริษัทระบุว่าจะดูแลรวบรวมและแก้ไขข้อผิดพลาดต่อไป โดยมีคณะกรรมการที่ปรึกษาซึ่งรวมทั้งสองคนนี้ ตลอดจน Dan Nakano ที่ปรึกษาภายนอก Axiom อธิบายว่าผลงานของบริษัทคือการทำให้สามารถตรวจสอบบทพิสูจน์ด้วยเครื่องจักรได้ จัดทำเอกสารบันทึกอุปสรรคที่พบ และเสนอข้อโต้แย้งที่ทำให้เป็นทางการเพื่อแก้ไขอุปสรรคเหล่านั้น พร้อมระบุว่าการจำแนกประเภทนี้ยังคงเป็นผลงานของนักคณิตศาสตร์ผู้ค้นพบกรุปและพัฒนาข้อโต้แย้งต่าง ๆ