On October 26, 2026, Axiom Math announced that it had put the classification of finite simple groups, one of the enormous theorems of mathematics, into a form that can be checked in the Lean proof assistant. The company worked on "formalization," which means writing mathematical definitions and proofs in a formal language that computers can process. According to Axiom Math, it produced about 43.1 million lines of code in 24 days. Along the way, it found a counterexample to an intermediate claim used in the traditional proof, but this does not overturn the classification of finite simple groups itself. To understand the achievement, it is important to distinguish three things: what can now be checked by machine, which inferences the counterexample affects, and where human verification is still needed.
The building blocks that appear when finite groups are broken down
There are 24 ways to rotate a cube so that it looks the same as before. Performing any two of these rotations in succession always gives one of the same 24, and each has an inverse that returns the cube to its original position. Group theory is the mathematical framework for this kind of structure, and a group with a finite number of elements is called a finite group.
When you decompose finite groups mathematically, you eventually reach building blocks that cannot be broken down further by the same method. These are simple groups. Strictly speaking, a simple group is a nontrivial group, not just the one consisting of the identity element alone, that has no normal subgroups other than itself and the trivial subgroup. The classification of finite simple groups is the theorem showing that all of these building blocks, which appear in every finite group, are contained in a known list. However, knowing the types of building blocks does not by itself make clear every way they can be combined to form a finite group.
The list includes cyclic groups of prime order and alternating groups of degree 5 or higher. It also includes families of groups called groups of Lie type, as well as 26 sporadic groups that belong to none of these families. The difficulty of the classification lies not only in discovering these groups one by one. The classification is complete only once it is proved that no finite simple group exists outside the list.
According to Axiom Math's announcement, the traditional human proof spans more than 500 papers and about 15,000 pages in total. The formalization targets this "first-generation proof," built over many years of mathematical research. In other words, it is not a new discovery of the classification result. The announcement describes the work as organizing arguments scattered across many papers into a single proof whose chain of dependencies, from the necessary premises to the final conclusion, can be checked by machine.
Existing code and human work behind the 24 days
The published code totals about 43.1 million lines, with roughly 2.05 million declarations, including definitions and theorems. However, the number of declarations does not directly equal the number of new mathematical discoveries. Most of it consists of existing mathematical knowledge written in a form computers can handle.
The 24 days of work also did not start from nothing. It built on Lean and the Mathlib mathematical library, as well as existing formalization work, including about 1.2 million lines from Qiuzhen-CFSG. According to Axiom Math's official report, the company's mathematicians and engineers ran dozens of AI agents, with the mathematicians analyzing obstacles in the proof and the engineers integrating and building the code. The work drew on accumulated research results and the expert efforts of people, so the 24 days cannot be simply compared with the decades of mathematical research that preceded it.
What matters in connecting the whole proof is less the amount of code than which premises each inference depends on. The company says it removed tens of thousands of lines of code that depended on unproven additional assumptions and rebuilt parts of its plan. Even if Lean confirms that a lemma holds under some assumption, the classification of finite simple groups has not been proved if that assumption itself cannot be proved. Individual proofs passing machine checks is a separate matter from being able to derive the final conclusion from only the necessary premises. The formalization also uncovered problems in the chain of inference within the traditional mathematical arguments.
What the PSL₂(49) counterexample refutes
A paper under Axiom Math's name, The Unbalanced Group Theorem, was released as a version 1 preprint on Hexagon on October 27, 2026. Its identifier is hexagon:2610.00575v1, and the registered contributors are Colin Defant and Ken Ono. Publication in a peer-reviewed journal has not been confirmed.
The paper's "Unbalanced Group Theorem" (UGT) is a theorem for narrowing down the type of an entire group from properties of subgroups inside a simple group. It concerns nonabelian simple groups and assumes inductively that the nonabelian simple composition factors appearing in their proper subgroups belong to the known classification. The paper calls this condition "K-proper." It is a condition for examining the smallest, in terms of number of elements, finite simple group that would exist if an unknown one did.
Suppose a group contains an "element of order 2," an element that returns to the identity when multiplied by itself. Collecting all elements whose result does not change when the order of multiplication with this element is swapped gives a subgroup called the centralizer. If that centralizer has a normal subgroup of odd order that is not just the identity, UGT shows that the original group belongs to either the groups of Lie type in odd characteristic or the alternating groups of degree 4a+3. Here a is a positive integer, and UGT is a theorem only about nonabelian simple groups satisfying the stated premises.
The counterexample found does not refute UGT itself. What the paper takes issue with is a "closure" claim used in John Walter's 1986 argument, in proving Proposition II.5.9(ii). Closure is the property that, when a particular operation is applied to a group belonging to a certain set, the simple components obtained still belong to that same set. The inference proceeded on the assumption that this property holds, but in fact there are examples that fall outside the set.
The specific counterexample is the group PSL₂(49). PSL₂ and PGL₂ are notations for types of groups, and the number in parentheses indicates the size of the finite field used in the construction. First, PSL₂(49) belongs to the set L0 specified in the paper. Next, consider an automorphism of order 2 arising from the structure of the finite field, that is, a transformation that permutes elements while preserving the group's operation structure. Collecting the elements fixed by this transformation gives a group isomorphic to PGL₂(7). Its simple component is PSL₂(7).
However, PSL₂(7) is not contained in L0. This is because 7 is a Mersenne prime, which the definition of L0 excludes. In other words, even starting from PSL₂(49), which belongs to L0, the specified operation produces a simple component outside the set. This shows that the closure required by the traditional inference does not hold in general. Note, though, that the automorphism used in this operation is not an element inside PSL₂(49), and so differs from the "element of order 2 within the group" that appears in the UGT conditions.
A single counterexample is enough to refute a mathematical claim that is supposed to hold in every case. But what this counterexample refutes is the closure claim used in Walter's proof, not the conclusion of Proposition II.5.9(ii) itself. In Remark 1.8, the paper also states explicitly that this counterexample is not a counterexample to the proposition or to UGT, but shows a flaw in an inference partway through the proof. What is needed, therefore, is not to change the conclusion of the classification but to replace the problematic inference with a valid argument.
An alternative proof route with explicit conditions
Can the necessary conclusion be derived without relying on the problematic closure? The paper builds an alternative proof route based on a theory published by Ronald Solomon in 1976. Its centerpiece is Theorem 2.3, "Preservation of simple tops." However, this is not a general principle that the type of the simple quotient is preserved for all groups and operations; it is a result with strict conditions on the groups and comparison operations involved.
First, the group G must be a nonabelian simple group satisfying the K-proper condition described above. The simple group T used as the basis of comparison is also restricted to either the alternating group A₇ of degree 7 or PSL₂(q), where q is an odd prime power of 5 or more. In addition, the choice of subgroups to be compared is subject to maximality conditions defined in the paper. Arbitrary subgroups cannot be freely compared.
Another important point is the assumption that "the 2-rank is 2" for every member of the family being compared. This means that the maximum order of an elementary abelian 2-subgroup, made up of mutually commuting elements of order 2, is 4. When all these conditions are met, Theorem 2.3 shows that the type of the corresponding simple quotient is preserved even when the comparison operations defined in the paper are repeated. The simple quotient here means the nonabelian simple group obtained from the group in question by removing normal subgroups of odd order and then dividing by the center. In other words, it is a result that maintains the type of the group only for specific comparison operations that satisfy the conditions, not one that applies to every operation.
The paper combines this theorem with reductions by Gilman and Solomon and with results by Foote and Harris for identifying the type of a group, and goes on to prove UGT for simple groups. Meanwhile, Remark 9.5 also describes a shorter proof route that derives UGT without using Theorem 2.3. Theorem 2.3 is therefore not the only means of supporting UGT. The paper keeps the long proof because it is the route AxiomProver actually formalized, and also because Theorem 2.3 itself contains results beyond what the proof of UGT requires.
This series of steps shows concretely what is at stake in formalizing mathematics. What matters is not only whether the final conclusion seems correct. One must make clear which intermediate claims fail to hold and by what argument, satisfying which conditions, they were replaced. The discovery of the counterexample and the change of proof route are an example of that process. However, the construction of a formal proof must be considered separately from a settled scholarly assessment of the meaning of the statements and of the paper as a whole.
The difference between machine checking and human verification
Axiom Math's official announcement explains that humans check whether the formalized statements and definitions correctly express the intended classification of finite simple groups, while Lean checks the formal inference leading to the conclusion. The README of the published GitHub repository also says that it uses standard axioms, contains no sorry (a placeholder for unproven parts), and does not rely on native_decide, which decides truth by running computations as native code. The build command for rechecking is given as lake build. Organizing the targets and roles of verification based on the published materials gives the following.
| Type of verification | What is verified | Published information and remaining items to confirm |
|---|---|---|
| Machine checking by Lean | Formal inference deriving statements from the stated definitions and premises | Described as using standard axioms and not depending on sorry or native_decide. What remains to be confirmed is whether third parties can rebuild the published code and reproduce the checking result. |
| Human check of meaning | Whether the statements and definitions correctly express the intended classification of finite simple groups | Stated explicitly by Axiom Math as the human role. Even if the formal inference is correct, whether the meaning of the statements matches the intent needs separate confirmation. |
| Scholarly review of the UGT paper | The scope of the claim the counterexample refutes, and the mathematical validity of the alternative proof | A version 1 preprint released on October 27, 2026, with no DOI assigned. Publication in a peer-reviewed journal and completion of a full independent third-party re-verification have not been confirmed. |
These are tasks that verify different problems. What machine checking guarantees is that, following the formalized premises and inference rules, the stated statements can be derived. If a statement different from the one humans intended had been formalized, a successful Lean check would not by itself mean the originally intended mathematical claim had been proved. Likewise, successfully rebuilding the published code is not the same as the mathematical argument in the UGT paper being scholarly verified.
Axiom Math reports that the formalization of the classification of finite simple groups is complete, but no report has been confirmed so far that an independent third party has finished re-verifying the entire published code. Going forward, it will be important for outside mathematicians and developers to scrutinize the formalized definitions and the final statement, and to see whether they can reproduce the checking result of the published code. Scholarly review by experts is also needed for the problem found in the proof of UGT and its alternative route.
The significance of this achievement lies in organizing a vast body of mathematical argument into a machine-checkable form and making explicit the problems found along the way and how they were resolved. Premises and chains of inference that were previously scattered across many papers can now be checked concretely by third parties. Through future independent verification, the reliability of the published formalization and the assessment of the mathematical results derived from it should become clearer.