💻 computer science

Lean-GAP: A Dataset of Formalized Graduate Algebra Problems

This paper introduces Lean-GAP, a dataset of 430 formalized graduate-level algebra problems from Dummit and Foote's textbook, along with a scalable pipeline for their creation and an analysis of the challenges and bottlenecks involved in translating informal mathematics into the Lean 4 proof assistant.

Original authors: Seewoo Lee, Byung-Hak Hwang, Hyojae Lim, Jihoon Hyun, Ilkyoo Choi, Yeachan Park, Jineon Baek, Hyukpyo Hong, Keewoo Lee, Jaeseong Heo, Hyungryul Baik, Chul-hee Lee, Kyu-Hwan Lee

Published 2026-06-03

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Seewoo Lee, Byung-Hak Hwang, Hyojae Lim, Jihoon Hyun, Ilkyoo Choi, Yeachan Park, Jineon Baek, Hyukpyo Hong, Keewoo Lee, Jaeseong Heo, Hyungryul Baik, Chul-hee Lee, Kyu-Hwan Lee

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

The Big Picture: Bridging Two Languages

Imagine you have a massive library of advanced math textbooks written in "Human Math" (informal language, diagrams, and standard notation). Now, imagine you want to translate every single problem in those books into "Robot Math" (a strict, computer-readable language called Lean 4).

Why? Because computers are getting very good at solving math problems, but they can only work if the problems are written in their strict language. Currently, there is a huge gap: we have tons of human math, but very little "Robot Math" for standard graduate-level courses.

The authors of this paper built a bridge across that gap. They created a dataset called LEAN-GAP, which contains 430 formalized algebra problems from a famous textbook (Abstract Algebra by Dummit and Foote).

The Process: A Three-Step Assembly Line

The team built a "factory" to turn human math problems into robot math. Here is how it worked:

The Scanner (PDF to LaTeX):
First, they took a scanned PDF of the textbook (which is just a picture of text) and used software to turn it into digital text code (LaTeX). Think of this like using a high-tech scanner to turn a handwritten letter into a typed document.
The Translator (Autoformalization):
Next, they used powerful AI models (like advanced chatbots) to translate that typed text into Lean 4 code. This is like asking a translator to turn a casual conversation into a legal contract. The AI tries to guess the right words and structure.
The Quality Control (Verification):
This is the most important and difficult part. Just because the AI produces code that the computer can read (it "compiles") doesn't mean the AI actually understood the math.
- The Analogy: Imagine the AI writes a sentence that is grammatically perfect but says the wrong thing (e.g., "The sky is green" instead of "The sky is blue"). The computer accepts the sentence, but the meaning is wrong.
- Because of this, the authors found that humans had to do the heavy lifting here. Mathematicians with PhDs and advanced students spent hours checking every single problem to ensure the "Robot Math" meant exactly the same thing as the "Human Math."

What They Found: The AI is Fast, but Human is Necessary

The team tested several different AI models to see which one was the best translator. Here are their main discoveries:

The "Compiler" Trap: Many AI models could write code that the computer accepted without errors. However, when humans checked the meaning, they found the AI often missed key details, flipped logic, or made up definitions that didn't exist.
The "Loop" Advantage: One AI system (Codex) that was allowed to try, fail, see the error message, and try again performed much better than the others. It was like a student who keeps practicing a math problem until they get the right answer, rather than just guessing once.
The "Human-in-the-Loop" Reality: Even the best AI couldn't do the job alone. The most time-consuming part of the project wasn't writing the code; it was the humans double-checking the code to make sure it was actually correct.

The Challenges: Where the Rubber Meets the Road

The paper highlights three specific types of problems that were very hard to translate:

Geometry Problems: Some problems involve drawing shapes with a compass and straightedge. It's very hard to teach a computer what a "drawing" is in a way that matches the human intuition.
"Find the Answer" Problems: Some questions ask you to list all possible answers. The AI sometimes just wrote down the answers as facts instead of setting up a problem to find them. The team had to restructure these so the computer had to actually solve the puzzle, not just read the solution key.
Missing Dictionary Words: Sometimes the textbook uses a specific math concept that doesn't exist in the computer's library (Mathlib) yet. The AI would try to guess a name for it, but the computer wouldn't know what that name meant. The humans had to build those definitions from scratch.

The Conclusion: A Team Effort

The paper concludes that while AI is getting better at translating math, we cannot rely on it to do the whole job alone yet.

Think of it like building a house:

The AI is like a robotic arm that can lay bricks very fast.
The Humans are the architects and inspectors who make sure the walls are straight and the house is safe.

The authors built a system where the AI does the heavy lifting of typing and initial translation, but humans remain in the loop to catch subtle errors. They hope that by sharing this dataset (LEAN-GAP), they can help train future AI systems to become better "math students," eventually helping them learn from standard textbooks rather than just solving tricky competition puzzles.

Technical Summary of LEAN-GAP: A Dataset of Formalized Graduate Algebra Problems

Problem Statement
Despite significant advances in automated reasoning and large language models (LLMs), a substantial gap remains between informal mathematical knowledge and its formal counterparts in proof assistants like Lean 4. While recent efforts have successfully formalized competition-style problems or highly specialized theorems, there is a scarcity of representative, structured datasets covering standard graduate-level material. This lack of foundational curriculum data hinders the development of automated reasoning systems, as they are often trained on "challenging problems" without the systematic conceptual development found in standard textbooks. Furthermore, while autoformalization has progressed, verifying that a generated formal statement faithfully captures the intended meaning of an informal statement remains a critical, unsolved bottleneck.

Methodology
The authors present LEAN-GAP (Lean-Graduate Algebra Problems), a dataset derived from 430 formalized exercises from the textbook Abstract Algebra by Dummit and Foote. The project employs a scalable, three-stage pipeline:

PDF-to-LATEX Preprocessing: Scanned PDF pages of the textbook are rendered as images, cropped to remove extraneous elements, and processed via the Mathpix Convert API to generate initial LATEX transcriptions of the exercise statements.
LATEX-to-Lean Autoformalization: A prompt-based approach using various LLMs translates the LATEX statements into Lean 4 code. The prompts enforce consistent naming conventions (e.g., DF_{sec}_{subsec}_{exercise_num}), compatibility with Mathlib, and the inclusion of sorry placeholders for proofs. The authors evaluated six systems: five single-shot models (GPT-5, Gemma4-31B, Goedel-Formalizer-V2-32B, Qwen3.6-35B-A3B, DeepSeek-R1-Distill-Qwen-32B) and an iterative agent loop (Codex).
Verification of Informal–Formal Correspondence: Recognizing that successful compilation does not guarantee semantic correctness, the authors implemented a rigorous human-in-the-loop verification workflow.
- Contributor Phase: A contributor rewrites the exercise as a self-contained theorem statement, formalizes it in Lean, and submits a Pull Request (PR).
- Automated Check: GitHub CI verifies that the Lean code elaborates against a pinned Mathlib revision.
- Maintainer Review: An independent maintainer performs a semantic review, ensuring the Lean declaration captures the mathematical content of the informal statement.
- AI-Assisted Correction: Tools like Claude Opus 4.7 and Aristotle are utilized as "second readers" to detect subtle semantic errors, such as flipped quantifiers or missing constraints (e.g., $n \ge 2$ ) that human reviewers might initially overlook.

Key Contributions

The LEAN-GAP Dataset: A structured corpus of 430 formalized graduate algebra exercises, organized by topic and difficulty, covering group theory, ring theory, field theory, and Galois theory.
Systematic Formalization Pipeline: A reproducible methodology for converting textbook exercises into formal statements, highlighting the necessity of human oversight in the verification stage.
Analysis of Formalization Challenges: A detailed examination of recurring bottlenecks, including:
- Geometric arguments: Exercises involving straightedge and compass constructions are difficult to formalize due to the lack of robust geometric infrastructure in Mathlib.
- Answer-embedded formalization: Problems requiring the enumeration of solutions pose challenges in distinguishing between verifying a given answer and discovering it.
- Missing definitions: Exercises requiring concepts not yet in Mathlib (e.g., specific Frobenius groups) necessitate custom definitions that must be carefully constructed to match the textbook's intent.
- Subtle ambiguities: Informal statements often contain implicit constraints (e.g., $n \ge 2$ ) that, if omitted, render the formal statement false in Lean's logic (e.g., due to natural number subtraction behavior).

Results
The authors evaluated the performance of different autoformalization models on the full set of 1,966 exercises:

Elaboration Success: Codex (an iterative agent loop) achieved the highest success rate at 95.5%, significantly outperforming single-shot models. GPT-5 led the single-shot models with 44.1% of exercises fully elaborating.
Semantic Fidelity: While syntactic success (elaboration) is necessary, it is not sufficient. An LLM-based semantic judge (Claude Opus 4.7) evaluated the faithfulness of the statements. GPT-5 achieved a mean score of 3.45/5, with 45.1% of outputs deemed "faithful." In contrast, DeepSeek-R1 scored significantly lower (1.15/5), often failing to emit declarations or producing vacuous statements.
Model Complementarity: The models exhibited high disagreement; only 7 exercises were solved by all systems, while 654 were solved by exactly one. This underscores the value of running models in parallel.
Human Verification Necessity: The verification stage proved to be the most labor-intensive. Even with high elaboration rates, many statements contained semantic errors (e.g., wrong group names, flipped quantifiers) that required expert human intervention to resolve.

Significance
The paper posits that LEAN-GAP addresses a critical gap in the training data for AI systems, moving beyond competition benchmarks to standard graduate-level curriculum. The work demonstrates that while LLMs can automate the initial translation of mathematical text, they cannot yet serve as end-to-end autoformalizers for standard material due to persistent semantic gaps. The authors argue that the future of formalization lies in productive human–AI collaboration, where AI acts as a "second reader" to identify subtle errors and unstated hypotheses, while human mathematicians provide the necessary oversight for semantic fidelity. This approach offers a template for scaling the formalization of standard mathematical training materials, potentially serving as a foundation for developing "AI mathematics students" capable of mastering standard curricula.