Pith. sign in

REVIEW 4 major objections 3 minor 75 references

FormaTheoria: Constructing Large-Scale Lean Theories from Mathematical Literature $-$ Toward the Formalization of the Classification of Finite Simple Groups

T0 review · 4 major / 3 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read FormaTheoria claims an AI workflow reconstructed a 994,000-line machine-checked Lean development of the Feit-Thompson, Glauberman Z-star, Brauer-Suzuki, and Bender-Suzuki theorems from the literature.

desk verdict A serious, genuinely new machine-checked Lean development covering major CFSG components, but the Bender–Suzuki claim rests on project-authored definitions and an LLM review that the authors admit is not proof of fidelity; treat it as conditional until the statement is independently audited. read the letter →

arxiv 2608.10894 v1 pith:ILSNXQ5J submitted 2026-08-11 cs.LO math.GR

Tianjiao Nie , Ao Zhang , Yusen Tang , Damiano Testa , Shing-Tung Yau , Peng Li , Yuan Zhou This is my paper · ORCID
classification cs.LOmath.GR MSC 03B3520D05
keywords FormaTheoriaLeanproofassistantautoformalizationtheoremprovingfinitesimplegroupsBender-SuzukiFeit-Thompsonlanguage-modelagents
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper claims that the remaining obstacle to formalizing the Classification of Finite Simple Groups is not proving individual theorems but reconstructing the surrounding theory from a scattered literature, and that an AI-assisted workflow can do this reconstruction at scale. To support the claim, it presents FormaTheoria, a pipeline that locates sources, translates definitions and statements into Lean, discovers missing dependencies recursively, constructs proofs through a graph of helper lemmas, independently reviews translations for mathematical fidelity, and reconciles conflicts between sources. Applied to the classification, the pipeline produced a machine-checked Lean development of more than 994,000 lines in more than 850 files that proves the Feit-Thompson Odd Order Theorem, Glauberman's $Z^*$ theorem, the Brauer-Suzuki theorem, and the Bender-Suzuki theorem. A sympathetic reader should care because, if the claim holds, a verified foundation for the full classification becomes a concrete continuation rather than a distant hope, and the workflow itself offers a template for formalizing other results whose proofs are dispersed across many independently written volumes.

What carries the argument

The load-bearing mechanism is the FormaTheoria workflow itself: a recursive pipeline of language-model agents that operate under a shared runtime with tool use, context compaction, and review-gated termination. Five components carry the argument: recursive on-demand dependency discovery, which suspends the current task, formalizes a missing prerequisite, and resumes; the PROVER procedure, which maintains a persistent directed acyclic graph of proved, proposed, and pruned helper lemmas across many model contexts; kernel-level statement immutability, enforced by hashing every declaration before and after each agent run; an independent semantic REVIEWAGENT, which compares each translation with the source in a fresh context and rejects elaborating-but-unfaithful statements; and RECONCILERAGENT, which repairs cross-source incompatibilities through local, source-supported bridges under an approval rule that forbids silently weakening approved statements. The root statements are additionally guarded by a comparator that checks the proved theorem's type against an independently written statement and verifies the axiom closure.

What would settle it

Sample a stratified set of approved declarations, concentrating on the reconciliation-heavy Peterfalvi Part I sections 10 and 13 where 192 of the 284 reconciliation modifications landed, have independent mathematicians compare each Lean statement against the source text without seeing the translator's reasoning, and look for a surviving mistranslation that changes the mathematical content while still compiling. The repository is public, so the audit is directly executable; one such confirmed mistranslation that passed both review and the comparator would break the semantic-fidelity premise.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is that a dependency-connected formal theory can be grown from a heterogeneous literature rather than assembled from a pre-specified blueprint: FormaTheoria starts from three human-selected books, recursively discovers the remaining sources it needs, and formalizes them into one coherent Lean development. The artifact is a repository of more than 994,000 lines whose verified theorems include the Feit-Thompson Odd Order Theorem, Glauberman's $Z^*$ theorem, the Brauer-Suzuki theorem, and the Bender-Suzuki theorem, with the Bender-Suzuki result stated as an equivalence between having a strongly embedded subgroup and belonging to one of three explicitly constructed matrix-group families. The paper presents this as evidence that AI-assisted workflows can reconstruct mathematically significant formal theories from distributed literature by combining language-model agents with formal verification, structured review, and explicit dependency management.

Load-bearing premise

The entire edifice rests on the premise that the language-model translation and review loop produces Lean statements that genuinely mean the theorems they are named after, since Lean itself only certifies well-typedness: the paper concedes that eventual acceptance by review does not prove that every translation choice is correct.

Editorial extensions

If this is right

  • The named continuation of the CFSG formalization is now a concrete program: the paper proposes the Gorenstein-Walter, Alperin-Brauer-Gorenstein, Gorenstein-Harada, and Aschbacher-Smith quasithin results as the next targets, with Gorenstein-Walter checkable against an externally fixed statement.
  • Formalization planning should follow the dependency graph rather than source page counts: the paper finds that page count correlates only weakly with formalization burden and that reconciliation work concentrates at a small number of representation-heavy interfaces.
  • Kernel verification becomes one layer of a larger quality system: the paper argues that well-typedness, semantic review, statement immutability, and root-statement comparison are each necessary and none sufficient alone.
  • The resulting repository offers stable, machine-checked interfaces: later formalization work can invoke the Bender-Suzuki classification and its predecessors without re-deriving their dependencies.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same four-challenge taxonomy plausibly transfers to other mathematically significant programs whose proofs are dispersed across independent volumes, and the lesson is that interface density, not page volume, predicts where integration will fail.
  • A testable extension the paper leaves implicit: run an automated refactoring pass over the generated code to merge ad hoc helper lemmas into Mathlib-style abstractions and measure how much of the 15-to-1 line-count ratio against the human-built version is compressible.
  • The strong statistical link between cross-section dependency counts and reconciliation modification rates suggests an early-warning instrument: projects could instrument interface density at section boundaries and use it to stage integration effort.
  • The fidelity evidence is stronger for the three theorems whose statements were fixed by an external benchmark than for the Bender-Suzuki statement, which the authors formulated; a fair stress test of the pipeline would target a theorem whose formal statement is fixed independently in a domain with no existing formalization.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 3 minor

Summary. The paper presents FormaTheoria, an AI-assisted workflow for constructing large-scale Lean formalizations from heterogeneous mathematical literature, and reports its application to major components of the Classification of Finite Simple Groups (CFSG). The workflow combines source retrieval and OCR, LLM-based translation, graph-based proof construction, recursive dependency discovery, independent semantic review, reconciliation of cross-source conflicts, and human escalation. The main empirical claim is that the workflow produced a machine-checked Lean development of more than 994,000 lines that proves formal statements of the Feit–Thompson Odd Order Theorem, Glauberman's Z* theorem, the Brauer–Suzuki theorem, and an equivalence that the paper names the Bender–Suzuki theorem. The paper also provides empirical analyses of dependency structure, source defects, reconciliation hotspots, and ablations of parallelization, context sharing, and review feedback.

Significance. If the claims hold, this is a significant milestone in formal mathematics: it would be the first machine-checked development of several deep results in finite-group theory, connected in one dependency graph, and it would demonstrate that AI-assisted workflows can reconstruct large theory bases from distributed literature. The paper deserves credit for emphasizing kernel verification, statement immutability, axiom checks, and a comparator for root statements, and for candidly discussing limitations of semantic review. The significance is, however, contingent on the semantic fidelity of the project-authored Bender–Suzuki statement: the formal theorem is machine-checked, but its identification with the literature theorem is not independently anchored.

major comments (4)
  1. [Appendix A, Theorem 5] The central claim that the development 'extends through the Bender–Suzuki theorem' rests on Theorem 5, whose statement is project-authored: the appendix says 'Theorem 5 has neither advantage. Its statement is ours.' The classification side of the equivalence is expressed through project-local constructions of PSL2(2^n), Sz(2^(2n+1)), and PSU3(2^n), and the reverse implication is proved only for those constructions. Since no external fixed statement or comparator anchors these definitions to the groups named in the literature, a subtle semantic drift in the constructions would make the machine-checked theorem a different theorem while still compiling. This is a load-bearing gap for the paper's headline claim and needs to be addressed, for example by an independently fixed statement of Theorem 5 in Mathlib vocabulary, explicit identification lemmas for each of the three families, or a carefully qualified claim in the abstract and conclusion.
  2. [Section 5.6 and Appendix A] The root-level checks using comparator are described as verifying that the proved theorem has the same type as an independently written statement and that the proof uses no extra axioms. However, Section 5.6 also states that these checks 'do not assess the source-level justification of intermediate declarations.' For Theorem 5 there is not even an independent root statement to catch semantic drift, because the statement is project-authored. The reader-facing sanity check of the reverse implication shows only that the project-defined groups admit strongly embedded subgroups, which is an internal property of those constructions and does not by itself establish that the constructions denote Suzuki's groups. I therefore do not see how the current evidence supports unqualified use of the name 'Bender–Suzuki theorem' in the abstract and introduction.
  3. [Section 3.3 and Section 6.3] Semantic fidelity is ultimately guaranteed by an LLM-based REVIEWAGENT with a self-improved rubric, and the pilot in Section 6.3 involves only ten source items with manual judgment of success. The paper's large-scale claims about 'preserving semantic fidelity' and the named theorems would be stronger if the authors provided either a larger, independent evaluation of accepted translations or an explicit statement that the external anchoring of Theorems 1–3 plus the project-authored statement of Theorem 5 is the intended epistemic status. This is not a request for perfection, but the scale of the development makes an n=10 pilot insufficient to support the semantic-fidelity component of the central claim.
  4. [Section 1.2 and repository link] The Lean code is said to be available at https://github.com/Qiuzhen-CFSG/CFSG, but the manuscript does not provide a commit hash, a snapshot date for the completed development, or explicit build instructions. Since the paper's central claim is that a specific machine-checked artifact exists, the artifact must be pinned and reproducible at the stated version. Without a commit hash, a reviewer cannot verify that the claimed 994,000-line snapshot corresponds to the code being described.
minor comments (3)
  1. [Appendix A, Theorem 3] The appendix states that Theorem 3 is displayed in a simplified but equivalent form and explains the equivalence informally; it would be helpful to state explicitly that this equivalence is not machine-checked and that the benchmark-fixed statement is the one in the LeanEval file.
  2. [Table 1 and Section 5.6] The comparison of code volume with Mathlib and the Rocq Odd Order development is explicitly described as not normalized, which is appropriate; however, the reader would benefit from a single table that also lists the commit or snapshot identifiers for each compared repository.
  3. [Section 6.1 and Section 6.2] The parallelization and context-sharing ablations report single runs per condition without variance or repeated seeds; the paper should state plainly that these are single-trajectory observations, not statistically repeated measurements, to avoid overgeneralizing the quantitative speedups.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the formalized theorems are anchored by Lean kernel checks and, for three of four, by fixed LeanEval statements; the project-authored Bender-Suzuki statement is a semantic-fidelity limitation, not a circular reduction.

full rationale

The paper's central claims are (a) a machine-checked Lean development of major CFSG components and (b) empirical claims about the workflow. For (a), the derivation chain is informal source -> formal Lean statement -> kernel-checked proof. The only step that could collapse into its own input would be if the formal statement were defined in terms of what is proved, or if the proof used the target as an axiom. Neither occurs: Section 5.6 and Appendix A report that the comparator checks root statements against independently written statements and replays proofs with no axioms beyond propext, Classical.choice, and Quot.sound. Theorems 1-3 are additionally pinned by LeanEval files 'a participant is forbidden to modify' (Appendix A). Theorem 5 is admitted to be project-authored ('Theorem 5 has neither advantage. Its statement is ours.'), but its hypothesis (strongly embedded subgroup) and conclusion (isomorphism to explicit PSL2/Sz/PSU3 constructions) are not defined in terms of each other; this is a semantic-correspondence risk, not a by-construction equivalence. For (b), the ablation studies and review statistics are empirical reports; the self-improved review rubric and the acknowledged absence of a fully independent gold standard (Section 5.5: 'eventual acceptance does not by itself prove that every remaining translation choice is correct') affect the strength of those reports, but they are not predictions whose values are fitted from the data they claim to validate. The citations to prior work by overlapping authors describe design antecedents and are not used to justify the mathematical results. No quoted equation or fitted parameter exhibits a self-definitional reduction, so no circular step is reported.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The mathematical statements are not derived with free parameters; they are formalizations of existing theorems. The unproved load is concentrated in semantic fidelity through LLM review and in the correctness of source-correction judgments. No new mathematical objects are postulated.

assumptions (4)
  • standard math Lean kernel and Mathlib foundation are consistent and correctly implement the logic used.
    The formalization relies on Lean 4 kernel checking and Mathlib declarations; the paper permits only propext, Classical.choice, and Quot.sound as axioms, as stated in Section 5.6.
  • domain assumption The natural-language mathematical sources are correct modulo the specific defects the workflow identifies and corrects.
    The workflow reconstructs proofs from Bender-Glauberman, Peterfalvi, Higman, Suzuki, Huppert, and others. Source defect corrections in Section 5.2 replace statements with the team's mathematical judgment, so the final theorems assert the corrected content rather than the literal source text.
  • ad hoc to paper LLM-based REVIEWAGENT semantic review is reliable enough that accepted Lean declarations faithfully represent the intended mathematical statements.
    Section 3.3 uses an LLM review with a learned checklist; Section 5.5 explicitly notes that eventual acceptance does not prove every translation choice correct, so faithfulness is an unverified assumption rather than a formally certified property.
  • domain assumption The explicit Lean constructions of PSL2(2^n), PSU3(2^n), and Sz(2^(2n+1)) faithfully encode the corresponding matrix groups from the literature.
    Appendix A grounds the Sz construction in Suzuki's paper and the PSU construction in Mathlib matrix vocabulary, but no independent formal specification of these constructions is provided outside the paper's own definitions.

how reviews work

0 comments
Cite this review

Pith. "Pith review of FormaTheoria: Constructing Large-Scale Lean Theories from Mathematical Literature $-$ Toward the Formalization of the Classification of Finite Simple Groups." pith.science (2026). https://pith.science/paper/ILSNXQ5J

@misc{pith2026260810894,
  author       = {Pith},
  title        = {Pith review of: FormaTheoria: Constructing Large-Scale Lean Theories from Mathematical Literature $-$ Toward the Formalization of the Classification of Finite Simple Groups},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ILSNXQ5J}},
  note         = {Machine review of arXiv:2608.10894}
}
abstract

Large-scale formalization of advanced mathematics requires more than translating individual statements: it must reconstruct a coherent theory distributed across heterogeneous sources. This process raises four challenges: discovering implicit dependencies, correcting source defects, preserving semantic fidelity, and reconciling cross-source misalignments. We present FormaTheoria, an end-to-end, AI-assisted workflow that coordinates source acquisition, formalization, proof construction, recursive dependency discovery, independent review, and reconciliation, while preserving provenance and protecting approved declarations. A shared agent framework supports long-horizon execution through tool use, context compaction, review-gated termination, section-level source context, and dependency-aware batch parallelization. Applying FormaTheoria to major components of the Classification of Finite Simple Groups (CFSG), we construct a machine-checked Lean development extending through the Bender--Suzuki theorem and encompassing the Feit--Thompson Odd Order Theorem, Glauberman's $Z^*$ theorem, and the Brauer--Suzuki theorem. This development verifies an extensive body of deeply interdependent finite-group theory while providing a foundation for continuing the CFSG formalization. An empirical analysis of the code and recorded construction process supports the practical relevance of the identified challenges and illustrates the roles of the corresponding workflow components. Together, these results demonstrate how AI-assisted workflows can reconstruct mathematically significant formal theories from distributed literature by combining language-model agents with formal verification, structured review, and explicit dependency management.

Figures

Figures reproduced from arXiv: 2608.10894 by the authors.

Figure 1
Figure 1. Overview of FORMATHEORIA. Starting from a root source item, the system retrieves and tran￾scribes the relevant source material, constructs a candidate Lean declaration, and, for a theorem, performs graph-based proof construction before independent review and approval. Newly discovered dependencies are formalized recursively, cross-source conflicts are handled by RECONCILERAGENT, and unresolved de￾pendencies, source … view at source ↗
Figure 2
Figure 2. Lean lines of code (LOC) against the number of source pages for all 46 rows in Table 3. The three [PITH_FULL_IMAGE:figures/full_fig_p026_2.png] view at source ↗
Figure 3
Figure 3. Distribution of the maximum path length starting from each project declaration in the Bender– [PITH_FULL_IMAGE:figures/full_fig_p028_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Source groups ordered by the share of declarations modified by R [PITH_FULL_IMAGE:figures/full_fig_p034_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

75 extracted references · 70 canonical work pages

  1. [1]

    Aristotle: IMO-Level Automated Theorem Proving.arXiv preprint arXiv:2510.01346, 2025

    Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathïs Fédérico, Sergei Gukov, Daniel Halpern- Leistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, et al. Aristotle: IMO-Level Automated Theorem Proving.arXiv preprint arXiv:2510.01346, 2025

    arXiv

  2. [2]

    Finite Groups with Quasi-Dihedral and Wreathed Sylow 2-Subgroups.Transactions of the American Mathematical Society, 151(1):1–261, 1970

    Jonathan L Alperin, Richard Brauer, and Daniel Gorenstein. Finite Groups with Quasi-Dihedral and Wreathed Sylow 2-Subgroups.Transactions of the American Mathematical Society, 151(1):1–261, 1970

    work page 1970

  3. [3]

    American Math- ematical Society, 2004

    Michael Aschbacher and Stephen D Smith.The Classification of Quasithin Groups. American Math- ematical Society, 2004

    work page 2004

  4. [4]

    Llemma: An Open Language Model for 44 Mathematics

    Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Qiaochu Jiang, Jia Deng, Stella R Biderman, and Sean Welleck. Llemma: An Open Language Model for 44 Mathematics. InProceedings of The Twelfth International Conference on Learning Representations (ICLR 2024), pages 40622–40649, 2024

    work page 2024

  5. [5]

    Growing Mathlib: Maintenance of a Large Scale Mathematical Library

    Anne Baanen, Matthew Robert Ballard, Johan Commelin, Bryan Gin-ge Chen, Michael Rothgang, and Damiano Testa. Growing Mathlib: Maintenance of a Large Scale Mathematical Library. In Proceedings of The 18th Conference on Intelligent Computer Mathematics (CICM 2025), pages 51–

    work page 2025

  6. [6]

    Transitive gruppen gerader ordnung, in denen jede involution genau einen punkt festläßt.Journal of Algebra, 17(4):527–554, 1971

    Helmut Bender. Transitive gruppen gerader ordnung, in denen jede involution genau einen punkt festläßt.Journal of Algebra, 17(4):527–554, 1971

    work page 1971

  7. [7]

    Cambridge University Press, 1994

    Helmut Bender and George Glauberman.Local Analysis for the Odd Order Theorem, volume 188. Cambridge University Press, 1994

    work page 1994

  8. [8]

    Springer Science & Business Media, 2013

    Yves Bertot and Pierre Castéran.Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer Science & Business Media, 2013

    2013

Show all 75 references
  1. [9]

    Beyond the Liquid Tensor Experiment

    Kevin Buzzard. Beyond the Liquid Tensor Experiment. Xena Project blog, 2022.https://xenapr oject.wordpress.com/2022/09/12/beyond-the-liquid-tensor-experiment/

    2022

  2. [10]

    Abstraction Boundaries and Spec Driven Development in Pure Mathematics.Bulletin of the American Mathematical Society, 61(2):241–255, 2024

    Johan Commelin and Adam Topaz. Abstraction Boundaries and Spec Driven Development in Pure Mathematics.Bulletin of the American Mathematical Society, 61(2):241–255, 2024

    2024

  3. [11]

    North-Holland, Amsterdam, 1982

    Walter Feit.The Representation Theory of Finite Groups, volume 25 ofNorth-Holland Mathematical Library. North-Holland, Amsterdam, 1982

    1982

  4. [12]

    Thompson

    Walter Feit and John G. Thompson. Solvability of Groups of Odd Order.Pacific Journal of Mathe- matics, 13(3):775–1029, 1963

    1963

  5. [13]

    Formal Proof--The Four-Color Theorem.Notices of the AMS, 55(11):1382–1393, 2008

    Georges Gonthier. Formal Proof--The Four-Color Theorem.Notices of the AMS, 55(11):1382–1393, 2008

    2008

  6. [14]

    A Machine-Checked Proof of the Odd Order Theorem

    Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A Machine-Checked Proof of the Odd ...

    2013

  7. [15]

    Harper & Row, 1968

    Daniel Gorenstein.Finite Groups. Harper & Row, 1968

    1968

  8. [16]

    American Mathematical Society, 1974

    Daniel Gorenstein and Koichiro Harada.Finite Groups Whose 2-Subgroups Are Generated by at Most 4 Elements, volume 147. American Mathematical Society, 1974

    1974

  9. [17]

    American Mathematical Society, Providence, RI, 1994

    Daniel Gorenstein, Richard Lyons, and Ronald Solomon.The Classification of the Finite Simple Groups, Number 1, volume 40.1 ofMathematical Surveys and Monographs. American Mathematical Society, Providence, RI, 1994

    1994

  10. [18]

    American Mathematical Society, Providence, RI, 1996

    Daniel Gorenstein, Richard Lyons, and Ronald Solomon.The Classification of the Finite Simple Groups, Number 2, volume 40.2 ofMathematical Surveys and Monographs. American Mathematical Society, Providence, RI, 1996. 45

    1996

  11. [19]

    American Mathematical Society, Providence, RI, 1999

    Daniel Gorenstein, Richard Lyons, and Ronald Solomon.The Classification of the Finite Simple Groups, Number 4: Part II, Chapters 1--4: Uniqueness Theorems, volume 40.4 ofMathematical Surveys and Monographs. American Mathematical Society, Providence, RI, 1999

    1999

  12. [20]

    The Characterization of Finite Groups with Dihedral Sylow 2-Subgroups

    Daniel Gorenstein and John H Walter. The Characterization of Finite Groups with Dihedral Sylow 2-Subgroups. I.Journal of Algebra, 2(1):85–151, 1965

    1965

  13. [21]

    The Characterization of Finite Groups with Dihedral Sylow 2-Subgroups

    Daniel Gorenstein and John H Walter. The Characterization of Finite Groups with Dihedral Sylow 2-Subgroups. III.Journal of Algebra, 2(3):354–393, 1965

    1965

  14. [22]

    The Characterization of Finite Groups with Dihedral Sylow 2-Subgroups—II.Journal of Algebra, 2(2):218–270, 1965

    Daniel Gorenstein and John H Walter. The Characterization of Finite Groups with Dihedral Sylow 2-Subgroups—II.Journal of Algebra, 2(2):218–270, 1965

    1965

  15. [23]

    The Formal Proof of the Kepler Conjecture: A Critical Retrospective.arXiv preprint arXiv:2402.08032, 2024

    Thomas Hales. The Formal Proof of the Kepler Conjecture: A Critical Retrospective.arXiv preprint arXiv:2402.08032, 2024

    2024 arXiv

  16. [24]

    A Formal Proof of the Kepler Conjecture

    Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. A Formal Proof of the Kepler Conjecture. InForum of mathematics, Pi, volume 5, page e2. Cambridge University Press, 2017

    2017

  17. [25]

    Hall, Marshall.The Theory of Groups

    Jr. Hall, Marshall.The Theory of Groups. Macmillan, New York, 1959

    1959

  18. [26]

    Finite Groups Having a Standard ComponentLof Type cM12 or cM22.Journal of Algebra, 319(2):621–628, 2008

    Koichiro Harada and Ronald Solomon. Finite Groups Having a Standard ComponentLof Type cM12 or cM22.Journal of Algebra, 319(2):621–628, 2008

    2008

  19. [27]

    HOL Light: An Overview

    John Harrison. HOL Light: An Overview. InProceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs ’09), pages 60–66. Springer, 2009

    2009

  20. [28]

    On Finite Groups Operating Doubly Transitively on Their Involutions.Archiv der Mathematik, 22(1):456–458, 1971

    Christoph Hering. On Finite Groups Operating Doubly Transitively on Their Involutions.Archiv der Mathematik, 22(1):456–458, 1971

    1971

  21. [29]

    Suzuki 2-Groups.Illinois Journal of Mathematics, 7(1):79–96, 1963

    Graham Higman. Suzuki 2-Groups.Illinois Journal of Mathematics, 7(1):79–96, 1963

    1963

  22. [30]

    MiniCTX: Neural Theorem Proving with (Long-) Con- texts

    Jiewen Hu, Thomas Zhu, and Sean Welleck. MiniCTX: Neural Theorem Proving with (Long-) Con- texts. InProceedings of The Thirteenth International Conference on Learning Representations (ICLR 2025), volume 2025, pages 10106–10130, 2025

    2025

  23. [31]

    Pessimistic Verification for Open Ended Math Questions

    Yanxing Huang, Zihan Tang, Zejin Lin, Peng Li, and Yang Liu. Pessimistic Verification for Open Ended Math Questions. InProceedings of the Forty-Third International Conference on Machine Learn- ing (ICML 2026), 2026

    2026

  24. [32]

    Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning.Nature, 651:607–613, 2026

    Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z Horváth, Goran Žuži ´c, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Masoom, et al. Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning.Nature, 651:607–613, 2026

    2026

  25. [33]

    Springer, 1967

    Bertram Huppert.Endliche Gruppen I, volume 134 ofDie Grundlehren der mathematischen Wis- senschaften. Springer, 1967

    1967

  26. [34]

    Springer, Berlin, Heidelberg, 1982

    Bertram Huppert and Norman Blackburn.Finite Groups III, volume 243 ofGrundlehren der mathe- matischen Wissenschaften. Springer, Berlin, Heidelberg, 1982. 46

    1982

  27. [35]

    Martin Isaacs.Character Theory of Finite Groups, volume 69 ofPure and Applied Mathematics

    I. Martin Isaacs.Character Theory of Finite Groups, volume 69 ofPure and Applied Mathematics. Academic Press, New York, 1976

    1976

  28. [36]

    Comparator.https://github.com/leanprover/comparator

    Lean FRO. Comparator.https://github.com/leanprover/comparator. Accessed 2026-08-11

    2026

  29. [37]

    LeanEval.https://github.com/leanprover/lean-eval

    Lean FRO. LeanEval.https://github.com/leanprover/lean-eval. Accessed 2026- 08-05

    2026

  30. [38]

    AI Mathematician: Towards Fully Automated Frontier Mathematical Research.arXiv preprint arXiv:2505.22451, 2025

    Yuanhang Liu, Yanxing Huang, Yanqiao Wang, Peng Li, and Yang Liu. AI Mathematician: Towards Fully Automated Frontier Mathematical Research.arXiv preprint arXiv:2505.22451, 2025

    2025 arXiv

  31. [39]

    The Lean 4 Theorem Prover and Programming Language

    Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. InProceedings of the 28th International Conference on Automated Deduction (CADE-28), pages 625– 635, Cham, 2021. Springer International Publishing

    2021

  32. [40]

    Paulson.Isabelle/HOL: A Proof Assistant for Higher-Order Logic

    Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson.Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, 2002

    2002

  33. [41]

    Le théorème de Bender–Suzuki I

    Thomas Peterfalvi. Le théorème de Bender–Suzuki I. InRévision dans les groupes finis: groupes du type de Lie de rang 1, number 142–143 in Astérisque, pages 141–233. Société mathématique de France, 1986

    1986

  34. [42]

    Cambridge University Press, 2000

    Thomas Peterfalvi.Character Theory for the Odd Order Theorem, volume 272. Cambridge University Press, 2000

    2000

  35. [43]

    Smith.Applying the Classification of Finite Simple Groups, volume 230

    Stephen D. Smith.Applying the Classification of Finite Simple Groups, volume 230. American Math- ematical Society, 2018

    2018

  36. [44]

    A Brief History of the Classification of the Finite Simple Groups.Bulletin of the American Mathematical Society, 38(3):315–352, 2001

    Ronald Solomon. A Brief History of the Classification of the Finite Simple Groups.Bulletin of the American Mathematical Society, 38(3):315–352, 2001

    2001

  37. [45]

    A New Type of Simple Groups of Finite Order.Proceedings of the National Academy of Sciences, 46(6):868–870, 1960

    Michio Suzuki. A New Type of Simple Groups of Finite Order.Proceedings of the National Academy of Sciences, 46(6):868–870, 1960

    1960

  38. [46]

    Springer, Berlin, Heidelberg, 1986

    Michio Suzuki.Group Theory II, volume 248 ofGrundlehren der mathematischen Wissenschaften. Springer, Berlin, Heidelberg, 1986

    1986

  39. [47]

    Release of Rocq 9.0.https://rocq-prover.org/changelog/ 2025-03-12-rocq-9.0, March 2025

    Rocq Development Team. Release of Rocq 9.0.https://rocq-prover.org/changelog/ 2025-03-12-rocq-9.0, March 2025. Accessed 2026-08-07

    2025

  40. [48]

    The Lean Mathematical Library

    The mathlib Community. The Lean Mathematical Library. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pages 367–381, New York, NY , USA, 2020. Association for Computing Machinery

    2020

  41. [49]

    DeepSeek-Prover: Advancing Theorem Proving in LLMs Through Large-Scale Synthetic Data.arXiv preprint arXiv:2405.14333, 2024

    Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek-Prover: Advancing Theorem Proving in LLMs Through Large-Scale Synthetic Data.arXiv preprint arXiv:2405.14333, 2024. 47

    2024 arXiv

  42. [50]

    Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Haowei Zhang, Qihao Zhu, Dejian Yang, Zhibin Gou, Z.F

    Huajian Xin, Z.Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Haowei Zhang, Qihao Zhu, Dejian Yang, Zhibin Gou, Z.F. Wu, Fuli Luo, and Chong Ruan. DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback fo...

    2025

  43. [51]

    LeanDojo: Theorem Proving with Retrieval-Augmented Lan- guage Models

    Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. LeanDojo: Theorem Proving with Retrieval-Augmented Lan- guage Models. InAdvances in Neural Information Processing Systems, volume 36, pages 21573...

    2023

  44. [52]

    FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models.arXiv preprint arXiv:2505.02735, 2025

    Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, et al. FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models.arXiv preprint arXiv:2505.02735, 2025

    2025 arXiv

  45. [53]

    MiniF2F: A Cross-System Benchmark for For- mal Olympiad-Level Mathematics

    Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. MiniF2F: A Cross-System Benchmark for For- mal Olympiad-Level Mathematics. InProceedings of The Tenth International Conference on Learning Representations (ICLR 2022), 2022. 48 A Formalized Theorems In this section we state ...

    2022

  46. [54]

    Import the narrowest module that exposes the declarations under study

  47. [55]

    Keep related checks and small examples together while the investigation is active

  48. [56]

    Run the probe from the repository root: lake env lean /tmp/<probe-directory>/Probe.lean

  49. [57]

    Read the complete diagnostic, revise one uncertainty, and rerun

  50. [58]

    error:|warning:|sorry|unsolved goals

    Put the final proof or definition in its owning module. Remove only temporary artifacts that you created. A successful probe establishes elaboration in the probe environment; it does not replace building the edited source module. Inspect declarations.Use exact qualified names ...

  51. [59]

    Restate the target in plain mathematical language: inputs, typeclass assumptions, hypotheses, and conclusion

  52. [60]

    Inspect the surrounding namespace, variables, imports, visibility, and neighboring proof style

  53. [61]

    Do not silently weaken, strengthen, or replace the claim

  54. [62]

    Loop for a proof

    Build the owning module before editing when a clean baseline is important. Loop for a proof

  55. [63]

    Normalize only enough to expose the mathematical shape withdsimp,simp, or carefully chosen rewrites

  56. [64]

    Search the local repository, then Mathlib, before proving reusable infrastructure from scratch

  57. [65]

    Confirm promising declarations with#checkor a small probe using the target imports

  58. [66]

    Keep theorem-local facts local or private; promote a helper to public API only when a real downstream consumer justifies it

    Decompose the proof into the smallest useful helpers. Keep theorem-local facts local or private; promote a helper to public API only when a real downstream consumer justifies it

  59. [67]

    Make a small source edit and runlake build <Target.Module>

  60. [68]

    Read the complete first error, inspect the local goal in a probe when needed, and fix one cause at a time

  61. [69]

    Use a fulllake build for final integration when the change crosses libraries or build configuration

    Once the owner builds, run the narrowest relevant downstream build. Use a fulllake build for final integration when the change crosses libraries or build configuration. Prefer disposableexampledeclarations over inserting exploratory placeholders into production source. If a to...

  62. [70]

    Build the owning module and relevant downstream target

  63. [71]

    Inspect logs forerror:,warning:,sorry, andunsolved goals; explain any pre- existing warning that remains relevant

  64. [72]

    Scan changed Lean source for unintendedsorry,axiom, andopaquedeclarations

  65. [73]

    Rebuild before using#print axioms Fully.Qualified.nameon exported theorems

  66. [74]

    Confirm intended names, namespace, visibility, imports, and statement meaning

  67. [75]

    Do not declare the task complete merely because a scratch example elaborates or one local theorem closes; satisfy the user’s full requested scope and integration boundary

    Rungit diff -checkand preserve unrelated working-tree changes. Do not declare the task complete merely because a scratch example elaborates or one local theorem closes; satisfy the user’s full requested scope and integration boundary. Long-horizon management The following inst...

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.