Axiom releases code for its claimed verification of a 15,000-page proof

Axiom Math says it has released computer-checkable code for the Classification of Finite Simple Groups (CFSG), whose written proof spans roughly 15,000 pages. Its October 26 announcement describes mathematicians and engineers directing dozens of agents for 24 days to produce 43.1 million lines of Lean code.

The project formalizes an existing mathematical achievement. Axiom reported 34 noteworthy departures from the literature, including missing hypotheses and arguments requiring repairs. Humans investigated consequential reports, consulting classification contributors Richard Lyons and Ronald Solomon.

The target proposition says every finite simple group is structurally equivalent to one explicitly constructed on the classification list. The referenced TauCeti file assembles cyclic, alternating, Lie-type and sporadic carriers, then defines that proposition. It explicitly records a statement to be proved, offering a precise starting point for reading what the larger development aims to establish. This equivalence concerns the group operation, allowing different names for elements.

An alternative route around a faulty inference

A companion paper examines a published argument toward the Unbalanced Group Theorem (UGT). Counterexamples refute closure under an operation for a specified family of simple groups. The paper distinguishes this failed inference from a counterexample to UGT or the intermediate proposition’s conclusion.

Using Solomon’s 1976 theory, the paper supplies an alternative argument for the classification’s simple-group case. Theorem 2.3 preserves associated simple quotients under specified comparisons and hypotheses. The longer formalized route and its additional result remain alongside a shorter human deduction in Remark 9.5.

The Apache 2.0 GitHub release describes a Lean 4.35.0-rc3 project built on Mathlib and TauCeti, using standard axioms without unproved placeholders. It also says it avoids native-code evaluation to decide propositions. These are the distributor’s descriptions of the verification setup.

The repository provides a build command. Axiom says open Lake build-tool changes and optimizations intended for upstream contribution brought its configured build below 24 hours. AI Ping compared release documentation with the pinned target statement but did not rebuild the full proof.

Lean’s official validation reference distinguishes checking a theorem from checking its dependencies. An imported result can contain an unproved placeholder even when a subsequent deduction passes. The documentation explains how to trace a theorem’s axioms and describes separate tools for checking compiled proofs again, extending scrutiny beyond an individual successful editor check.

The reference also separates valid formal deduction from the meaning of a statement. A machine checks conclusions against supplied definitions and premises; understanding whether those definitions express the intended mathematics requires reading the specification. Third-party examination of the release therefore has both a formal verification target and a mathematical specification to inspect.

The proof website separates the initial agent blueprint from the Lean repository view. Readers can search statements and milestones and explore dependencies by paper or stage. Its errata page still said on October 28 that group theorists were compiling the list for future publication. The complete curated correction list was therefore still forthcoming. The site counts 715 papers and books and about 2.05 million declarations, including definitions and theorems. Its views organize the corpus by source works and statements, helping readers navigate connections within the release.