Axiom Formalizes Largest Math Proof in Lean in 24 Days

Axiom used swarms of AI agents guided by mathematicians to auto-formalize the Classification of Finite Simple Groups, a proof spanning approximately 15,000 pages and 500 papers, into roughly 40 million lines of Lean code in 24 days. Axiom said earlier this year getting its prover to write a correct 10,000-line Lean proof took weeks; this task was about 4,000 times larger. Axiom attributes the capability jump to simultaneous improvements across models, its agent harness, and infrastructure. Separately, a company called Resolution (formerly Sequent) used a single-researcher-orchestrated agent system to formalize Hironaka's resolution of singularities in Lean, producing 600,000 lines of formal proof at a cost of roughly $135,000 in tokens over about one week, consuming approximately 100 billion input tokens and 300 million output tokens. Resolution said the formalized library is already being used to extend singular learning theory and understand model generalization.