Axiom Math, an artificial intelligence startup based in Palo Alto, says it completed in 24 days the first fully computer-checked formalization of the Classification of Finite Simple Groups, a monumental theorem spanning approximately 15,000 pages. Its AxiomProver system translated the argument into the Lean language, generating approximately 43.1 million lines of code and creating the largest Lean codebase to date. The process corrected more than 2,000 errors in the existing literature, including 34 notable deviations, and closed a significant gap in the Unbalanced Group Theorem. The formalization confirms that the list of finite simple groups is complete, while the multi-agent system was overseen by expert mathematicians.
Source: Read the original article
