Summary (Overview)

• LEAN-GAP is a dataset of 430 formalized graduate-level algebra problems from the textbook Abstract Algebra by Dummit and Foote, representing over 20% of the textbook's 1,966 exercises.
• The authors develop a scalable three-stage pipeline: PDF-to-LaTeX preprocessing, LaTeX-to-Lean autoformalization via LLMs, and human-in-the-loop verification of informal–formal correspondence.
• Key finding: Verification is the most labor-intensive and subtle step—LLMs can elaborate syntactically correct Lean code that is semantically wrong, and no automated method reliably checks informal–formal correspondence.
• Model evaluation: GPT-5 leads single-shot models with 44.1% elaboration success; Codex (agent loop) achieves 95.5% via compiler-grounded retries, but semantic faithfulness remains low across all models (best mean score 3.56/5).
• The dataset is organized by topic, difficulty, and structural features, with permission from the copyright holder (John Wiley & Sons) for non-commercial research use.

---

Introduction and Theoretical Foundation

The paper addresses a critical gap in formal mathematics: while proof assistants like Lean 4 have enabled major formalization efforts (Liquid Tensor Experiment, Prime Number Theorem, Fermat's Last Theorem), most existing benchmarks focus on competition-style problems rather than standard graduate-level curriculum material.

The authors draw an instructive analogy:

"An instructive analogy is that of attempting to train a student using only challenging problems, without first guiding them through the standard curriculum typically covered in the first years of graduate study."

Motivation: The scarcity of representative, structured datasets for graduate-level mathematics hinders both AI training and the development of automated reasoning systems. The textbook by Dummit and Foote is chosen because:

• It is one of the most widely adopted graduate algebra texts
• Its exercises are integral to the exposition, not merely supplementary
• Exercises introduce important ideas through carefully organized sequences

Theoretical challenge: Formalizing informal mathematics requires resolving implicit assumptions, contextual dependencies, and ambiguity. The paper emphasizes that successful compilation does not guarantee semantic correctness—a Lean file may elaborate yet encode a different mathematical statement.

---

Methodology

Pipeline Architecture

Stage 1: PDF-to-LaTeX Preprocessing

• Render textbook pages as images using pdftoppm (Poppler library)
• Crop extraneous elements (running titles, page numbers)
• Process with Mathpix Convert API (OCR service for STEM documents)

Stage 2: LaTeX-to-Lean Autoformalization

• Prompt-based LLM translation with a structured prompt enforcing:
  • Consistent naming convention: DF_{sec}_{subsec}_{exercise_num}
  • No extra variable definitions (all included in statement)
  • import Mathlib assumed, no submodule imports
  • Output as theorem statements with by sorry placeholders
  • Subproblems (a), (b), (c) formalized as separate theorems

Stage 3: Two-Stage Human Verification Each exercise passes through:

1. Contributor prepares the formalization
2. GitHub CI checks elaboration against pinned Mathlib revision
3. Independent maintainer reviews semantic correspondence

Per-exercise workflow:

1. Selection from Git repository
2. Informal rewrite: Exercise rephrased as self-contained theorem statement with all hypotheses inlined
3. Formalization: Lean statement produced (directly or LLM-assisted)
4. Pull request: ≤10 exercises per PR
5. Independent review: Maintainer checks semantic correspondence, resolves disagreements
6. Merge: Declaration + informal rewrite become dataset entries

Autoformalization Models Evaluated

Six systems were tested:

• Single-shot baselines: GPT-5, Gemma4-31B (think), Goedel-Formalizer-V2-32B, Qwen3.6-35B-A3B, DeepSeek-R1-Distill-Qwen-32B
• Agent loop: Codex (GPT-5 backbone) with compiler-grounded retries

---

Empirical Validation / Results

Elaboration Outcomes (Table 1)

Key observations:

• GPT-5 leads single-shot models (44.1%), benefiting from scale
• Goedel-Formalizer-V2-32B's autoformalization-specific fine-tuning helps (36.2%)
• DeepSeek-R1's chain-of-thought traces consume output budget (1,040 missing)
• Codex's compiler feedback loop closes most of the gap (95.5%)

Error Distribution (Table 2)

Dominant error categories across models:

• unknownIdentifier: hallucinated names (most common)
• synthInstanceFailed: missing typeclass instances
• invalidField: incorrect field access

Semantic Evaluation (Table 3)

LLM-judge (Claude Opus 4.7) scoring on five axes: mathematical objects (S1), hypotheses (S2), conclusion (S3), structure (S4), specificity (S5).

Critical insight: Goedel-Formalizer has the highest all-pass elaboration count among single-shot models but lower semantic quality than GPT-5—syntactic success ≠ semantic correctness.

Cross-Model Analysis

• Only 7 exercises solved by every system; 654 by exactly one—strong argument for parallel model deployment
• 60 universally failed exercises cluster in advanced chapters (39/60 in Chapters 10–18), reflecting Mathlib coverage gaps rather than model weakness
• Even Codex ceilings at 95.5%; remaining failures stem from Mathlib drift (renamed lemmas, restructured instances) since model training

---

Theoretical and Practical Implications

Challenges in Formalization

1. Geometric arguments: Exercises on straightedge-and-compass constructions (e.g., regular 17-gon in Chapter 14.5) resist formalization—the notion itself requires significant infrastructure not in Mathlib.

2. Answer-embedded formalization: For enumeration problems (e.g., "find the order of each element in ℤ/12ℤ"), the paper proposes:

def DF_1_1_11_ans : Fin 12 → ℕ
    | 0 => sorry
    | 1 => sorry
    | 2 => sorry
    ...
theorem DF_1_1_11 : ∀ i : ZMod 12, addOrderOf i = answer i := by

This avoids the "verification-only" trap while requiring a Python script to prevent hacking (e.g., defining answer i := addOrderOf i).

3. Missing Mathlib definitions: For $F_{20}$ (Frobenius group), the authors define it via generators and relations:

inductive Generators | u | v deriving DecidableEq, Repr
open FreeGroup in
def F20 := PresentedGroup {
    (of Generators.u)^4,
    (of Generators.v)^5,
    (of Generators.u) * (of Generators.v) * (of Generators.u)^(-1 : ℤ) * (of Generators.v)^(-2 : ℤ)
}

4. Faulty original statements: The paper found a case (Exercise 21, Chapter 2.3) where the textbook itself was imprecise—the claim $(1+p)^{p^{n-2}} \not\equiv 1 \pmod{p^n}$ requires $n \geq 2$, which Aristotle [1] exposed via counterexample $(n,p) = (1,3)$. In Lean, natural subtraction gives $1 - 2 = 0$, making the statement false without the additional hypothesis.

Human-AI Collaboration Model

The paper advocates for AI as second readers rather than standalone formalizers:

• Claude Opus 4.7 caught a reversal error in $(a_1 a_2 \cdots a_n)^{-1} = a_n^{-1} a_{n-1}^{-1} \cdots a_1^{-1}$
• Aristotle found counterexamples to flawed statements

---

Conclusion

Main takeaways:

1. Current LLMs cannot be relied upon as end-to-end autoformalizers for graduate-level mathematics—even with high elaboration rates, semantic fidelity remains poor
2. Verification is the fundamental bottleneck, requiring mathematical expertise and careful human oversight
3. The pipeline offers a template for productive human-AI collaboration in formalization

Future directions:

• Complete formalization of remaining ~1,536 exercises through community participation
• Generate informal–formal pairs of solutions via automated theorem provers
• Develop an "AI mathematics student" benchmark for standard curriculum material
• Use LEAN-GAP as an educational resource for integrating formal methods into mainstream mathematical practice

Key quote:

"Progress depends on the joint evolution of the original mathematics material, the underlying formal library, the evaluation infrastructure, and the model itself."

The dataset will be publicly released with copyright permission from John Wiley & Sons for non-commercial research and educational purposes.