# Axiom Says AI Agents Machine-Checked the Classification of Finite Simple Groups in 24 Days

The 43.1-million-line Lean 4 formalization corrected more than 2,000 errors in the literature and required new proof work to close a gap in the Unbalanced Group Theorem, according to the company.

- Published: 2026-10-28T06:21:21.801Z
- Canonical: https://polylog.news/ai/2026-10-28/axiom-says-ai-agents-machine-checked-the-classification-of-f
- Publisher: Polylog (AI desk)
- Section: tech
- Sources: [Polylog editors](https://polylog.news)

Axiom Math said on October 27 that it has completed a computer-checked proof of the Classification of Finite Simple Groups (CFSG) in the Lean proof assistant, [the Russian-language channel AI ML Big Data reported](https://t.me/ai_machinelearning_big_data/11225). The original proof runs to roughly 15,000 pages across more than 500 articles by about 100 mathematicians, written over several decades. Axiom says engineers and mathematicians directed swarms of dozens of AI agents over 24 days. The agents wrote about 43.1 million lines of Lean 4, [according to Unite.AI](https://www.unite.ai/axiom-math-releases-43-1m-line-lean-proof-of-group-classification/). The company has [published the code on GitHub](https://cryptobriefing.com/axiom-ai-formalizes-enormous-theorem-24-days/) under an Apache 2.0 license.

The most substantive claim concerns errors. Axiom says the process found and corrected more than 2,000 errors in the existing literature, 34 of which it classifies as notable deviations. It also says it found a significant gap in the Unbalanced Group Theorem and wrote a new section of proof to close it. If independent group theorists confirm that gap, the project will have produced new mathematics, not merely a translation of existing proofs. The company also describes the output as the largest Lean codebase ever created. That description is Axiom's own, and no independent count has been published.

Three points need independent checking before the result can be treated as settled. First, the top-level Lean statement must match what mathematicians mean by the theorem. A formalized statement that is subtly weaker than intended can still pass Lean's check while proving the wrong thing. Second, the codebase must be free of placeholder gaps, known in Lean as `sorry` statements, and of non-standard axioms. Lean's own tooling can audit both automatically. Third, the 24-day figure excludes earlier infrastructure work and the human direction that Axiom itself acknowledges. Other groups are working toward the same goal. The [FormaTheoria workflow, posted to arXiv in August,](https://arxiv.org/pdf/2608.10894) coordinates AI-assisted formalization with independent review, and a [Renaissance Philanthropy-backed modular human-AI program](https://www.renaissancephilanthropy.org/modular-humanai-approach-to-classification-of-finite-simple-groups) also targets CFSG. Those projects give the field reviewers who can audit Axiom's claim.

## What this means

The method here has AI agent swarms writing proofs that a small, trusted kernel checks. That addresses the core weakness of large language model reasoning, which is output that cannot otherwise be verified. When the checker is mechanical, the cost of being wrong falls on the agent's compute bill rather than on a human reviewer's time. The approach suits any domain with a formal checker, starting with mathematics and extending to hardware verification, smart-contract audits and safety-critical code. Vendors of formal-methods tools and the chip and avionics firms that pay for verification are the most exposed, because their main constraint is a shortage of human verification engineers. Many observers will read this as a mathematics milestone. The larger signal is that machine-checkable output at the scale of tens of millions of lines is now a product category. The precedent is the four-color theorem: a computer-assisted proof from 1976 met years of skepticism until a formal Coq verification in 2005 settled it. The likelier outcome this time is a much shorter audit, on the order of weeks to months, because Lean's kernel check can be rerun by anyone. The question that matters is whether the top-level statement is faithful to the theorem. If group theorists confirm the statement and the Unbalanced Group Theorem gap, expect labs to market formal verification of code and hardware within months. A finding that the top-level statement is weaker than CFSG would prove this read wrong.

## What to watch

- Whether independent group theorists confirm the Lean statement of the main theorem. Their sign-off determines whether the 43.1 million lines prove what Axiom says they prove.
- Whether the published repository passes a public audit for placeholder proofs and added axioms. That check can be done mechanically, and a clean result would remove the main technical doubt.
- Whether Axiom or a competitor announces formal verification of a large industrial codebase or chip design. That would show the method moving from mathematics into paid engineering work.