Axiom Math, a startup based in Palo Alto, has utilized its multi-agent AxiomProver system to complete the first computer-verified formalization of the Classification of Finite Simple Groups. The original proof, known as the Enormous Theorem, spans approximately 15,000 pages and incorporates work from over 100 mathematicians across more than 500 papers.
The process involved translating the mathematical arguments into the Lean programming language, resulting in a codebase of approximately 43.1 million lines. This achievement marks the largest Lean codebase created to date. The system's work was conducted over a period of 24 days and was supervised by expert mathematicians.
During the verification, the system identified and corrected over 2,000 errors in the existing literature, including 34 notable deviations. The team also addressed a significant gap in the Unbalanced Group Theorem by developing a new segment of proof. The company is led by CEO Carina Hong, with mathematician Ken Ono serving as a key figure.
Earlier this year, the AxiomProver system reportedly solved open mathematical conjectures and achieved a perfect score on the Putnam exam. The Classification of Finite Simple Groups categorizes these groups into four types: cyclic of prime order, alternating groups, 16 families of groups of Lie type, or one of 26 sporadic groups.
