Kingy AI
Subscribe, 2.1M subscribersWork with Kingy
AI News

Axiom Says AI Formalized a 15,000-Page Math Proof in 24 Days

October 27, 2026 Blog
Geometric symmetry illustration beside Axiom’s reported figures: about 15,000 pages of human mathematics, 24 days, and 43.1 million lines of Lean code.

Axiom Math says its AI agents, working with mathematicians and engineers, have formalized one of mathematics’ largest existing proofs in Lean in 24 days. The company has released the source code for its claimed formalization of the Classification of Finite Simple Groups, a theorem whose human proof grew across decades and hundreds of papers.

The scale is hard to absorb. Axiom estimates that the traditional proof spans roughly 15,000 pages and draws on work by around 100 mathematicians. The project is exciting because it tackles a connected body of mathematics, with definitions and dependencies stretching across an enormous literature. Its public release gives other mathematicians a concrete artifact to examine and build on.

There is a significant qualification. Axiom describes the formalization as complete, but its project metadata identifies the review as self-assessed. We have not reproduced the build or conducted an independent mathematical audit. The 24-day figure is the company’s account of the formalization project, not a measure of the decades of human work behind the theorem or all the earlier software it uses.

The announcement, dated October 26, describes a human-guided effort in which agents wrote and revised formal proofs while the team handled mathematical obstacles and engineering infrastructure. A separately released paper dated October 27 examines a problem in one published route through the classification and presents an alternative argument.

What was classified?

A group is a mathematical way to describe operations that can be combined. The operations must follow a few rules: combining them stays within the group, there is an identity operation, each operation has an inverse, and the order in which combinations are grouped does not change the result.

Picture a square. Rotate it by 0, 90, 180 or 270 degrees, and it still occupies the same outline. Those four rotations form a group: two 90-degree turns have the same effect as one 180-degree turn, and a 270-degree turn reverses a 90-degree turn. The language of group theory makes such relationships precise, whether the objects are geometric shapes or more abstract structures.

A finite group has a finite number of elements. A finite simple group is a nontrivial one with no proper nontrivial normal subgroup. Normality is a specific condition that makes a subgroup suitable for breaking the larger group down; a simple group can still have plenty of subgroups that are not normal.

Our four rotations are not a simple group. The 0-degree and 180-degree rotations form a normal subgroup inside it. For a simple example, take the five rotations of a regular pentagon through multiples of 72 degrees. They form a cyclic group of prime order five.

Simple groups are often compared with prime numbers because they appear as building blocks in a finite group’s composition series. The analogy has limits. The resulting simple factors, including their multiplicities, are independent of the composition series chosen, but those factors alone do not uniquely tell us how to reconstruct the original group. The extension problem, figuring out how pieces fit together, remains a separate task.

The list is finite in form, not in size

The classification says that every finite simple group belongs to an established list, up to isomorphism: in this context, the same group structure can have different labels for its elements. The usual accounting gives 18 infinite families and 26 exceptional sporadic groups. The families include cyclic groups of prime order, alternating groups, and 16 families of groups of Lie type. An introduction to sporadic groups describes that counting convention, while the ATLAS lists the sporadic examples.

“Infinite families” matters here. The theorem does not say there are only 44 finite simple groups. Each family contains groups described by parameters, and the classification’s sweeping claim is that no finite simple group falls outside the list. It does not classify every finite group, and it does not claim to classify all infinite simple groups.

Establishing that exhaustive claim took an extraordinary human effort. Proofs appeared across a sprawling literature, and the classification developed over much of the twentieth century. Michael Aschbacher’s account of the final quasithin contribution places its publication in 2004. The story includes later work to reorganize and clarify parts of the proof, as well as the original discoveries.

What does it mean to formalize a proof?

Mathematical papers use a mixture of symbolic argument, prose and shared background. Experienced readers fill in steps and check that references apply. A formal proof has to express the definitions, theorem and every required deduction in a language a proof assistant can check.

Lean is one such proof assistant. Its kernel checks that a proposed proof follows from the definitions and permitted logical foundations. When a theorem depends on earlier results, those dependencies also matter. This makes a formal development valuable as a connected library: a later proof can refer to precise statements whose dependencies are available for inspection.

Checking has a boundary. A proof assistant verifies the proposition it has been given under its foundations; people still need to judge whether the formal definitions and final statement express the mathematical claim they intended. A flawlessly checked proof of a weakened statement would not settle the stronger one.

Axiom’s public repository supplies a solution theorem tied to an explicit classification statement. The project’s metadata names the main results and lists three permitted standard axioms: propositional extensionality, classical choice and quotient soundness. The Lean documentation explains these foundations and how to inspect a theorem’s axioms. Axiom says its final development has no unfinished proof placeholders and does not use native_decide. Those are project claims; we have not independently traced all dependencies.

One detail illustrates why the exact artifact matters. The repository includes a challenge template containing a deliberate placeholder as well as a separate solution file. A search for the placeholder’s text across the whole repository would therefore be a poor substitute for checking the final theorem and its dependencies.

The human work came first

This project builds on an existing theorem and earlier formal mathematics. Axiom’s third-party documentation credits work including Mathlib, Tau Ceti and other group-theory formalizations. The 24-day clock does not capture the creation of those libraries or the original mathematics.

A useful comparison is the odd-order theorem, an important part of the classification story. In 2012, Georges Gonthier and collaborators completed a machine-checked proof in Coq after roughly six years of work, according to Microsoft Research’s account. Their 2013 paper describes the resulting proof and libraries. The odd-order theorem says that every finite group of odd order is solvable: it can be broken down through a chain whose successive factors are abelian groups, in which the operation commutes. One consequence is that every nonabelian finite simple group has even order and contains an involution. That makes it possible to investigate such groups through involution centralizers. The Coq achievement formalized this major theorem, rather than the whole classification.

More recent projects also advanced pieces of the task. The FormaTheoria preprint describes formal work on several substantial components, while a Constructive ATLAS preprint describes constructions of families and sporadic groups. Constructing examples and proving that the list contains every possible example are different jobs.

These milestones show how much infrastructure and mathematical knowledge had already accumulated. They do not support a clean speed comparison: the projects had different scopes, tools, resources and starting points.

How Axiom organized the agents

Axiom describes coordinated agents, human intervention and shared infrastructure. Its account includes discarded conditional proofs and efforts to reduce repeated computation.

That coordination is a substantial part of the story. An isolated proof can be checked on its own, but a classification depends on thousands of statements fitting together. Definitions must agree across files. A result one agent needs must have the exact assumptions another has established. A change deep in the dependency tree can affect work far away.

The public project page displays approximately 43.1 million Lean lines, 2.05 million declarations and 100 milestones. These are Axiom’s reported project statistics; we have not recounted them. The team has not disclosed the total compute cost, hardware, complete model inventory or person-hours in the primary material we reviewed. Twenty-four elapsed days should not be read as a complete accounting of effort.

A repair in the mathematical literature

The project also led Axiom to examine arguments in the human literature. Its October 27 Unbalanced Group Theorem paper identifies what it says is a false closure assertion used in one route to a result, and offers a replacement argument.

At a high level, the theorem relates local information about certain elements and their centralizers to the structure of a larger finite group. An involution is an element of order two; its centralizer is the collection of elements that commute with it. These local structures help mathematicians reason about the possible shape of the whole group.

The paper gives a counterexample to the particular closure assertion by examining an automorphism of a group called PSL₂(49). It then develops an alternative comparison argument using ideas from earlier work. The distinction matters: a defective step in one argument does not by itself refute the Unbalanced Group Theorem, the classification, or every other proof route. The paper explicitly discusses other routes as well.

The paper is public and available for specialists to scrutinize. Its host, Hexagon, says that it does not conduct peer review or judge correctness or novelty on acceptance.

What happens next

Formal mathematics can make long chains of reasoning easier to reuse and inspect. If independent reviewers confirm that this development checks and that its statement captures the intended classification, mathematicians could use it as a foundation for further formal work. That is a promising implication of a public, interconnected library, not a measured productivity gain already established by the release.

The next checks are concrete. Researchers can try a clean build, inspect the final theorem’s transitive assumptions, examine the definitions behind the classification statement and review the mathematical arguments, including the proposed repair. The repository provides build instructions; Axiom says a full build can take under 24 hours with its described Lake changes and optimizations. We have not verified that timing or reproduced the build.

For AI, the compelling claim is sustained work across a web of dependent mathematics, under human direction and with proof-checking tools providing exact feedback. For mathematics, the opportunity is a public artifact that specialists can challenge, check and eventually use. The external scrutiny now deserves as much attention as the announcement.