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

> FORMATHEORIA formalized the Classification of Finite Simple Groups in Lean at 994,000+ lines, exposing source defects and achieving 4.2x speedup via dependency-aware parallelism.

- **Source:** [arXiv](https://arxiv.org/abs/2608.10894)
- **Published:** 2026-08-17
- **Permalink:** https://picx.dev/p/UQ23ax
- **Whiteboard:** https://picx.dev/p/UQ23ax/image

## Summary

# 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:

| Development | Formal system | Reported scale | Source organization |
|---|---|---|---|
| Mathlib | Lean | 1.9M lines (2025) | General-purpose library |
| Odd Order | Rocq | ~150K lines | One theorem from two expositions |
| Flyspeck | HOL Light & Isabelle | ~500K lines | One proof with project-specific blueprint |
| Liquid Tensor | Lean | ~90K lines | One theorem via shared blueprint |
| **FORMATHEORIA** | **Lean** | **>994K lines, 850+ files** | **Heterogeneous literature requiring discovery** |

## 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.\text{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

| Experiment | Key Result |
|---|---|
| Parallel vs. Sequential | Wall time reduced 76.1% (4.2×); tokens increased 45.7% |
| Context Sharing | Wall time reduced 26.5%; total tokens reduced 18.0% |
| Review Feedback | 6/10 → 10/10 correct translations with self-improved rubric |

### 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.

---

_Markdown view of https://picx.dev/p/UQ23ax, served by PicX — AI-generated visual whiteboard summaries of research papers._