Startup Axiom says its multi-agent system AxiomProver fully formalized the Classification of Finite Simple Groups (CFSG)—the “Enormous Theorem”—into Lean in about 24 days, producing ~43.1 million lines, claimed larger than the Linux kernel and other major open-source trees. The run logged hundreds of anomalies, including ~34 major logical gaps, and against a closure claim in Walter’s 1986 Unbalanced Group Theorem (UGT) argument produced a counterexample, then—with Richard Lyons and Ronald Solomon—formalized a new result, Preservation of simple tops, as a patch. If independently verified, it would mark AI moving from checker to co-author of a repair theorem at the top of pure math—treat the claim as pending audit of the repo and peer review. Related: ETH-refutation claims and Meta’s large Lean library.
Why CFSG Is “Enormous”
Groups encode symmetry; finite groups factor into finite simple groups. CFSG is the “periodic table”: cyclic of prime order, alternating on ≥5 letters, 16 Lie-type families, and 26 sporadics (largest: the Monster). From the 1950s, ~100 mathematicians across 500+ papers built ~15,000 pages; Gorenstein’s 1983 “done” still had a hole filled in 2004 by Aschbacher–Smith (~1,221 pages). Length makes human end-to-end reading and zero-error writing nearly impossible—hence formalization.
24-Day Swarm: Map, Lean, Infra Bottlenecks
Per Axiom, work started Oct 1, 2026 on Slack; humans split the proof into ~108 milestones and ~380 tasks. From Oct 2, agents decomposed hard lemmas, searched, wrote Lean, and outsourced missing prerequisites into a shared library. Throughput briefly overwhelmed Lean dependency checks until engineers added distributed caching. By Oct 10 they reported formalizing that the Monster is simple; total ~24 days and ~43.1M Lean lines. Emotional posts (e.g. Ken Ono) are testimony, not a substitute for technical audit. More: AI News.
Human–AI Patch: UGT Breaks, New Theorem Lands
Phrases like “obviously” fail in Lean. Beyond typos, ~34 major deviations appeared; a critical one sat in UGT (local subgroup structure → global type). Formalizing Walter 1986, agents rejected a key closure claim and gave counterexample PSL₂(49) (Mersenne-prime-7 exclusion cases). Rather than restart on a full “second-generation” proof, the team looped in Lyons and Solomon, sketched a path from Solomon’s 1976 ideas, and had AxiomProver formalize Preservation of simple tops to recover the needed UGT form—conclusion intact, proof path now AI-patched. The motive echoes Voevodsky’s turn to machine checking: complex arguments outrun unaided human review.
FAQ
Q: Does formalizing CFSG mean the theorem was only now proved? A: No. Humans completed the classification over decades; this is machine-checkable Lean formalization plus gap-finding and repair.
Q: What does “largest open-source project” mean? A: Axiom’s Lean line-count vs Linux et al.—verify against the public repo and counting method; lines ≠ scientific impact.
Q: Did AI alone discover new math? A: Per the account, humans and the system co-designed the repair route; AxiomProver supplied the tight formalization—best framed as human–AI collaboration pending papers/repo.
相关文章
