งานวิจัย
Axiom ใช้ฝูง AI agent formalize การจำแนกกรุปเชิงเดียวจำกัด (CFSG) ลง Lean ครบใน 24 วัน — 43.1 ล้านบรรทัด ไม่มี sorry และระหว่างทางเจอจุดผิดในบทพิสูจน์ที่ตีพิมพ์ตั้งแต่ปี 1986
Axiom Math ประกาศเมื่อ 26 ต.ค. 2026 ว่าใช้ฝูง AI agent หลายสิบตัว ภายใต้การกำกับของวิศวกรและนักคณิตศาสตร์ formalize บทพิสูจน์รุ่นแรกของ Classification of Finite Simple Groups ลง Lean 4 ได้ครบใน 24 วัน ได้โค้ด 43.1 ล้านบรรทัด ไม่มี sorry ใช้แค่ axiom มาตรฐาน 3 ตัว และใช้ statement จากโปรเจกต์ TauCeti ภายนอก ระหว่างทางพบ 34 จุดที่เบี่ยงจากเอกสารที่ตีพิมพ์ รวมถึง counterexample ต่อข้ออ้างในบทพิสูจน์ Unbalanced Group Theorem ปี 1986 รีโปเปิดภายใต้ Apache-2.0
· อ่าน 5 นาที