Deyron Labs graphic: Axiom Math Lean formalization of the classification of finite simple groups; 43.1M lines, 2.05M declarations, per Axiom's project page

What happened

Axiom Math has published a project page for a Lean formalization of the first-generation proof of the classification of finite simple groups (CFSG), a result the page describes as spanning thousands of journal pages written by about a hundred mathematicians. The page is undated; aggregator coverage placed the announcement on 27 October 2026.

Key details

  • Size (Axiom’s figures): 43.1 million lines of Lean and 2.05 million declarations.
  • Verification claim: the page states that every logical step is checked by Lean’s kernel. We have not independently run or audited the code.
  • Deviation from the literature: the authors say they found an issue in a published argument for the Unbalanced Group Theorem and used an alternative route, which an accompanying paper explains. Some secondary coverage cites larger numbers of deviations and a 24-day build time; we could not find either on the project page, so we do not report them.
  • People: the page names Dean Cureton, Vasily Ilin, Bhavik Mehta and Niels Voss as core contributors and Letong Hong as principal investigator.
  • Page inconsistencies: the page lists 100 milestones in one place and 108 in another, and the source counts differ between sections, so exact totals should be treated as approximate.

Why it matters

Machine-checked proofs of very large human arguments are one of the clearest tests of AI-assisted mathematics, because a proof checker, not the model, decides whether it is correct. If the formalization stands, it would make a famously long and hard-to-audit proof checkable end to end. For now this is Axiom’s own presentation: the date, build process and the extent of AI involvement are not documented on the page, and mathematicians have not yet reviewed whether the Lean statements faithfully capture the theorem.

Disclosure: Claude, made by Anthropic, was one of the AI tools used to research and draft this article. Details come from Axiom’s project page, read on 28 October 2026.

Sources

  1. Classification of Finite Simple Groups in Lean (Axiom Math project page) Primary source , Axiom Math