Summary

Summary (Overview)

• FORMATHEORIA is an end-to-end, AI-assisted workflow for large-scale formalization of mathematics from distributed literature, specifically targeting the Classification of Finite Simple Groups (CFSG).
• The workflow coordinates source acquisition, formalization, proof construction, recursive dependency discovery, independent review, and reconciliation while preserving provenance and protecting approved declarations.
• The authors constructed a Lean formalization exceeding 994,000 lines across 850+ files with 30,298 declarations reachable from the Bender–Suzuki theorem, encompassing the Feit–Thompson Odd Order Theorem, Glauberman's Z* theorem, and the Brauer–Suzuki theorem.
• Dependency-aware parallelism reduced proof-construction wall time by 76.1% (4.2×), section-level context sharing reduced wall time by 26.5% and token consumption by 18.0%.
• The work identifies four core challenges (C1–C4): distributed sources with deep dependencies, cross-source misalignments, semantically incorrect Lean translations, and defects in mathematical sources.

Introduction and Theoretical Foundation

Background and Motivation

Formal mathematics represents definitions, statements, and proofs in languages checkable by a small trusted kernel. The Classification of Finite Simple Groups (CFSG) presents a unique challenge: its proof is distributed across a large, historically layered literature whose dependencies, definitions, conventions, and representations must be recovered and aligned during formalization.

By the Jordan–Hölder theorem, simple composition factors of a finite group are determined up to isomorphism and reordering. CFSG identifies all finite simple groups: cyclic groups of prime order, alternating groups, groups of Lie type, and sporadic groups. The proof emerged over decades from approximately one hundred mathematicians and remains dispersed across hundreds of papers and books.

Four Core Challenges

C1: Distributed sources and deep dependencies. The source corpus comprises numerous books and papers rather than a single self-contained exposition. Dependencies frequently cross source boundaries, and cited results may depend on substantial chains of earlier results.

C2: Misalignments across mathematical sources. Different sources may define the same object under different conventions, introduce extensionally equivalent formulations through distinct constructions, or use the same name for different objects.

C3: Semantically incorrect Lean translations. A Lean declaration may elaborate successfully while misrepresenting the source—omitting assumptions, mistranslating quantifiers, or strengthening/weakening conclusions. Lean's elaborator establishes well-typedness, not semantic fidelity.

C4: Defects in the mathematical sources. Sources may contain typographical errors, missing conditions, ambiguous formulations, incomplete arguments, or incorrect statements.

Comparison with Existing Work

The paper contrasts FORMATHEORIA with major formalization projects:

Methodology

Formalization Model

For a source item $s$, a formalization is a tuple:

$$f_s = (\text{type}_s, \text{term}_s, \Gamma_s, \text{state}_s),$$

where $\Gamma_s$ is a Lean context, $\text{type}_s$ is a Lean type, and $\text{term}_s$ is a Lean term satisfying:

$$\Gamma_s \vdash \text{term}_s : \text{type}_s.$$

The state is:

$$\text{state}_s \in \{\text{candidate}, \text{approved}\}.$$

Workflow Components

Algorithm 1: FORMATHEORIA (simplified):

1. Retrieve source material via SEARCHAGENT and OCRAGENT
2. Translate via TRANSLATORAGENT
3. If theorem, iteratively run PROVER
4. Handle MissingDependency recursively, Conflicts via RECONCILERAGENT
5. Escalate Failures to human investigation

Shared Agent Framework

The framework operates as:

$$\text{AGENTFRAMEWORK}(p, \mathcal{R}) \longrightarrow o$$

where $p$ is a task prompt and $\mathcal{R}$ is a review agent. Key features include:

• Multi-turn LLM interaction with tool use (read, edit, write, bash)
• Context compaction when token length exceeds threshold $B_{\text{ctx}}$
• Review-gated termination: stop points trigger review; rejection adds diagnostic feedback to context

PROVER Procedure

The PROVER uses a directed acyclic graph $G_s$ with nodes having states:

$$a.\mathrm{prover\_state} \in \{\text{proposed}, \text{proved}, \text{pruned}\}.$$

PROVEAGENT attempts proofs; REFINEAGENT decomposes "TooHard" obligations into helper lemmas. Statement immutability is enforced via kernel-level declaration hashing.

Issue Classification

• Source defects: [DEF1] errors in statements, [DEF2] errors in proofs
• Source misalignments: [MAL1] equivalent but not definitionally equal formalizations, [MAL2] same name for different objects
• Incorrect translations: [INT1] unprovable incorrect translations, [INT2] translations that fail in downstream applications

Empirical Validation / Results

Scale and Structure

• 15 books/papers consulted covering 1,037 pages
• Only 3 sources (357 pages, 34.4%) were initially supplied; dependency discovery added 12 sources (680 pages, 65.6%)
• 30,298 project declarations and 186,187 edges in the Bender–Suzuki closure
• Root theorem depth: 458 (Bender–Suzuki), 430 (Feit–Thompson)
• Median depth: 2; 29.4% of declarations have depth zero; 99th percentile: 378

Source Defects and Misalignments Found

The workflow identified several mathematical issues in the literature:

1. Incompatible definitions of type I maximal subgroups [MAL1]: Bender–Glauberman requires a condition for all complements, while Peterfalvi requires only existence of one complement. Resolved via Schur–Zassenhaus equivalence bridge.

2. Typographical error in type I maximal subgroup definition [DEF1]: $O_{p'}(M)$ should be $O_{p'}(H)$ in Bender–Glauberman's condition (Iv)(c).

3. Missing condition in Peterfalvi [DEF1]: Appendix IV Lemma 2(c) requires $|Q_1|$ odd, omitted from statement.

4. Error in Huppert's Theorem 8.27 [DEF1]: The divisibility condition $t \mid \frac{p^{\hat{m}}-1}{d}$ should be $t \mid p^m - 1$ and $t \mid \frac{p^f-1}{d}$.

5. Indexing error in Higman's Lemma 11 [DEF2]: Basis $u_0, \ldots, u_m$ should be $u_0, \ldots, u_{m-1}$.

Reconciliation Concentration

• 284 of 10,417 declarations (2.7%) modified by RECONCILERAGENT
• PF Part I Sections 9, 10, 13 account for 219 modifications (77.1%)
• Modification share correlates with cross-section dependency count: Pearson $r = 0.861$, Spearman $\rho = 0.820$ (both $p < 0.001$)

Review Outcomes

• 11 of 14 PF Part I sections returned after first review (78.6%)
• 16 rejected outcomes total; 30 review rounds required
• Pilot study: 6/10 correct without review, 7/10 with binary decision, 9/10 with diagnostics, 10/10 with self-improved rubric

Ablation Results

Comparison with Rocq Formalization

• Lean: 573,050 lines vs. Rocq: 39,163 lines in shared BG/PF Part I sections (ratio ~15:1)
• Both developments verify the Odd Order Theorem with kernel-level checks and no unauthorized axioms
• Different proof routes: Lean proves Glauberman's theorem on $Z(J(S))$ directly; Rocq follows Puig's theorem via BG's Appendix B

Theoretical and Practical Implications

For Formal Mathematics

The work demonstrates that large-scale formalization requires reconstructing theory, not just proving statements. The declaration dependency graph reveals a "broad shallow base connected to root theorems through a narrow but exceptionally deep backbone"—a structure that must inform workflow design.

For AI-Assisted Proof

The results show that semantic fidelity requires review beyond kernel verification. Lean's elaborator establishes well-typedness but not source fidelity. The review agent's checklist (recovering inherited context, preserving canonical data, avoiding strengthening for convenience) proved essential for translation quality.

For Mathematical Literature

The formalization effort exposed actual defects in published mathematics, including typographical errors, missing hypotheses, and incorrect statements in standard references (Huppert, Higman, Peterfalvi, Bender–Glauberman). This demonstrates formalization's value as an auditing tool for mathematical literature.

Design Principles

1. Dependency-aware parallelism converts inference capacity into reduced elapsed time (4.2× speedup)
2. Section-level context sharing amortizes context reconstruction costs across related tasks
3. Constrained reconciliation (local, source-supported repairs) is more effective than unrestricted refactoring
4. Human escalation should be reserved for cases where automated workflow cannot determine a source-based continuation

Conclusion

FORMATHEORIA successfully demonstrates 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. The completed formalization of major CFSG components—extending through Bender–Suzuki and encompassing Feit–Thompson, Glauberman Z*, and Brauer–Suzuki—represents a significant milestone toward the full formalization of the Classification of Finite Simple Groups.

Future Directions

1. Continue CFSG formalization: Gorenstein–Walter theorem, Alperin–Brauer–Gorenstein theorem, Gorenstein–Harada theorem, Aschbacher–Smith work
2. Dynamic scheduling: extend batch parallelism with dynamic assignment, critical-path prioritization, and interface conflict detection
3. Code quality improvement: refactoring into stable abstractions, aligning with Mathlib, improving readability
4. Formalization-backed knowledge base: interactive interfaces exposing definitions, provenance, dependencies, and proof structure to help mathematicians navigate CFSG's extensive prerequisites

The work establishes that the principal challenge in large-scale formalization is not proving individual statements but constructing the dependency-connected theory required to state and prove target results, with quality control requiring mechanisms beyond kernel checking alone.