Axiom Says AI System Formalized 15,000-Page Group Theory Proof
Photo: TokenPost
Axiom Math announced Oct. 26 that its AxiomProver system completed a formal version of the Classification of Finite Simple Groups that can be checked by computer. The company described the work as the first complete formalization of the result. The original proof spans about 15,000 pages and draws on more than 500 papers. More than 100 mathematicians contributed to the proof over several decades. Axiom’s effort took 24 days and produced about 43.1 million lines of Lean code. Lean is a language for expressing mathematical claims and proofs in a form a computer can check.
Source: TokenPost
