Axiom says AI agents verified math’s longest proof in Lean

Axiom Math says it has produced the first complete computer-checked proof of the classification of finite simple groups, a result the company calls the longest proof in the history of mathematics. In an Oct. 26 post, Axiom said engineers and mathematicians at the startup directed “swarms of dozens of AI agents” over 24 days to write about 43.1 million lines of code in Lean, a programming language in which a computer checks every step of a proof.

What was formalized: The classification, known by its initials CFSG, lists every finite simple group, the building blocks from which all finite groups are assembled. Axiom said the original human proof spans roughly 15,000 pages in more than 500 articles by about 100 mathematicians. The company said it chose to formalize the “first generation” proof, the version whose last major gap was closed in 2004, because the reorganized “second generation” proof remains incomplete. Axiom said its Lean development covers the existence and simplicity of the listed groups and the proof that every finite simple group appears on the list.

How it worked: Axiom said it opened a Slack channel on Oct. 1 and split the project into 108 milestones and about 380 smaller tasks drawn from a proof map built from the published literature. The first agent swarm went live Oct. 2. Agents claimed milestones through GitHub issues, lead agents broke down hard arguments and reviewed statements, and human mathematicians investigated obstructions, the company said. On Oct. 10, Axiom said, the channel announced that the agents had proved the Monster, the largest of the 26 sporadic groups, is simple. Axiom said the work builds on Mathlib, Lean’s community math library, and incorporates about 1.2 million lines from a project called Qiuzhen-CFSG.

What the agents found: Axiom said translating the literature into Lean exposed mostly minor problems, such as typos, table errors and dropped hypotheses, but also 34 “noteworthy deviations from the published record.” The largest involved the Unbalanced Group Theorem: Axiom said its agents found counterexamples to a closure assertion in John Walter’s 1986 memoir. The company said those counterexamples did not refute the theorem itself. It said its AxiomProver system produced an alternative argument, including a new result it calls “Preservation of simple tops,” drawing on ideas from mathematician Ronald Solomon. Axiom said it consulted Solomon and Richard Lyons, two group theorists who worked on the original classification, and that it will release an errata list.

Who checked it: The claims are Axiom’s own, and the company’s post cites no independent review. Axiom said that Lean checks the deductions, while humans must inspect the final formal statement and its definitions to confirm they express the intended classification. Ken Ono, a number theorist the post lists among the project’s contributors, is Axiom’s founding mathematician and is on leave as a professor of mathematics at the University of Virginia, according to his university page. Axiom said its release documents how readers can check the development.

Why it matters: This claim is different in kind from the one two AI labs made on Tuesday about the exponential time hypothesis. That work claimed new results; Axiom says it checked a theorem mathematicians have accepted for decades. That is where machine checking is easiest to judge, because the target is known and Lean either accepts the proof or it doesn’t. The open question is the one Axiom itself names: whether the formal statement matches the classification as mathematicians mean it, and that takes human eyes. Axiom’s list of 34 deviations is the part outside group theorists can test now, since each item points to a specific published argument. If those hold up, the project shows AI agents doing large-scale proof checking that took human experts decades to organize. Until outside experts weigh in, it remains a company’s account of its own work.