AI news Oct 29, 2026

This week · research page, October 26

Axiom says its agents formalized a 15,000-page proof

AI math company Axiom says its agents turned a 15,000-page proof into Lean code a machine can check, in 24 days, and people checked that the theorem was stated correctly

Why it matters: Our inference: if Axiom's account holds, putting a long existing proof into Lean, a program that checks proofs step by step, now takes weeks, and what mathematicians still have to check is whether the theorem is stated correctly.

Axiom, an AI math company, announced on its research page on October 26 that teams of AI agents had completed a Lean formalization of the first-generation proof of the classification of finite simple groups. The theorem lists every finite simple group.

What Axiom did is translate an existing proof into a form a machine can check, not produce a new proof. The original proof runs about 15,000 pages and was completed over generations by about 100 mathematicians. Axiom turned it into about 43.1 million lines of code that the Lean theorem prover can check step by step. The first agent teams went live on October 2, and the work took 24 days, with Axiom's engineers and mathematicians directing dozens of agent teams. The research page doesn't say which model was used, or how many lines people and machines each wrote (Axiom research page, 2026-10-26).

Lean guarantees that each step from premises to conclusion is valid. It cannot tell whether the premises and conclusion say what the original theorem means, so a person has to read them. The research page says people checked the statement of the main theorem and the definitions it uses, confirming that the statement expresses the intended classification, while Lean checked the formal derivation of the main theorem. The work turned up 34 deviations from the published literature, listed on a separate errata page; the research page doesn't say whether each one is a typo or a gap. The code repository is public, and its README states there are no unfinished placeholders and only three standard axioms are used (GitHub AxiomMath/CFSG).

Not proven yet: everything is Axiom's own account; no independent team has reported a successful build How we checked →

Next to watch: whether the Lean community or Mathlib maintainers publish a build report. If any independent team's build fails, finds unfinished placeholders, or shows the main theorem's statement doesn't match the standard definition, "completed" has to be withdrawn.