FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels

AI summary

Overview

Research area: Machine learning for formal mathematical theorem proving, specifically benchmark construction and evaluation for large language models working in the Lean proof assistant.

Technical level: Advanced. The paper assumes familiarity with interactive theorem provers, Lean 4, the Mathlib library, abstract and commutative algebra, and LLM evaluation metrics such as pass@64.

Scope: The paper introduces and evaluates FATE-H and FATE-X, two 100-problem formal algebra benchmarks at graduate and PhD-qualifying-exam difficulty, and analyzes why state-of-the-art LLMs fail on them.

What This Paper Is About

Existing formal theorem-proving benchmarks for LLMs focus on competition problems (like the IMO) and introductory university mathematics, which do not reflect the depth and abstraction of modern mathematical research. The authors build a graded algebra benchmark series stretching from undergraduate exercises to problems beyond PhD qualifying exams, and then measure how the strongest available LLMs and specialized provers perform on it. The central question is whether current models' successes on contest math transfer to research-level formal mathematics.

Key Contributions

1. Progressive benchmark creation. The paper introduces FATE-H and FATE-X (100 problems each) and extends the existing FATE-M benchmark from 141 to 150 problems, forming the complete FATE series across undergraduate to post-PhD qualifying exam difficulty in abstract and commutative algebra. The authors state that FATE-X is the first formal benchmark to surpass both PhD qualifying exam difficulty and Mathlib's formalization coverage.

2. Baseline performance evaluation. A comprehensive evaluation of general reasoning models (o3, Gemini-2.5-Pro, Claude-4-Sonnet-thinking, DeepSeek-R1, Qwen3) and specialized theorem provers (DeepSeek-Prover-V2-671B, Kimina-Prover-72B, Goedel-Prover-72B), establishing that the best model achieves only 3% (pass@64) on FATE-H and 0% (pass@64) on FATE-X.

3. Two-stage output analysis. The authors observe that models generate natural-language reasoning before formalizing it, then separately evaluate each stage. They find natural-language accuracy far exceeds formalization accuracy, and classify common formalization errors into four categories: Mathlib hallucinations, Lean proficiency issues, general capability issues, and misalignment.

4. Comparative study of reflection. A qualitative comparison of DeepSeek-V3, DeepSeek-Prover-V2, and DeepSeek-R1 (all post-trained from the same base model) identifies "effective reflection" — the ability to locate, diagnose, and repair flaws — as the capability separating the general reasoning model from the specialized prover.

Main Findings

• Steep collapse across difficulty levels. On FATE-M, models score between 16.0% (Qwen3-235B-A22B-Thinking) and 62.7% (DeepSeek-Prover-V2-671B). On FATE-H, only o3 (3.0%), DeepSeek-Prover-V2-671B (3.0%), Goedel-Prover-V2-32B (2.0%), and Kimina-Prover-72B (2.0%) solve anything. On FATE-X, every model scores 0.0%.

• Human baseline sets the difficulty gradient. In a controlled human experiment, algebra PhD students and postdocs each received 5 non-overlapping natural-language problems from FATE-H and FATE-X with 2.5 hours to solve them. They achieved 73% on FATE-H and 21% on FATE-X.

• Expert validation of difficulty. In a questionnaire with ten professors from top institutions specializing in algebra, 7/10 said the FATE problems were either directly appropriate for algebra/commutative algebra qualifying exams or notably more challenging than standard PhD qualifying exam questions. Experts consistently rated FATE significantly higher than classical textbooks and ProofNet in difficulty, coverage, and originality.

• The bottleneck is formalization, not mathematics. DeepSeek-R1 reaches 71.0% natural-language (pass@1) accuracy on FATE-H versus 0.0% formal (pass@64), and 33.0% versus 0.0% on FATE-X. DeepSeek-Prover-V2 reaches 39.0% natural language versus 3.0% formal on FATE-H, and 9.0% versus 0.0% on FATE-X. Goedel-Prover-V2 reaches 48.0% versus 2.0% on FATE-H and 8.0% versus 0.0% on FATE-X. Kimina-Prover reaches 35.0% versus 2.0% on FATE-H and 3.0% versus 0.0% on FATE-X.

• Error categories, ranked by frequency. For mathematically correct but formally incorrect attempts on FATE-H, Mathlib hallucinations (35/39 for DeepSeek-Prover-V2, 70/71 for DeepSeek-R1) and Lean proficiency issues (36/39 and 70/71) were the most common. General capability issues apart from headers occurred at intermediate frequency (19/39 and 18/71), and misalignment was the least common (3/39 and 0/71).

• New definitions are required. 38% of FATE-X problems need definitions not present in Mathlib, formalized before the problem statement, averaging 2.4 new definitions each, including concepts such as local complete intersections and Gorenstein rings. Models rarely generated auxiliary lemmas for these problems.

• Specialized provers reflect less effectively. DeepSeek-Prover-V2 was confined to "formal reflections" such as starting over or a rhetorical shift without a corresponding logical change, and showed non-aligned behaviors including questioning the correctness of the problem statement after a failure and "conscious cheating behaviors." Its intermediate natural-language accuracy ended up close to DeepSeek-V3's, while DeepSeek-R1 significantly outperformed both.

• Most models solve in two stages. All models with visible reasoning content (DeepSeek-R1 and all theorem provers) produced a full natural-language proof before formalizing, even without being instructed to. Gemini-2.5-Pro and Claude-4-Sonnet-thinking also reasoned in natural language first, while o3 directly output formalization attempts.

Methodology in Plain English

The authors assembled a benchmark by hand rather than scraping it. They gathered 400 candidate algebra problems and split them into two 200-problem pools at hard and expert difficulty, with a four-day collaborative curation involving nearly twenty postdocs and PhDs in pure algebra. Sources included more than 20 standard undergraduate and graduate textbooks (such as Lang and Eisenbud), publicly available PhD qualifying exams, honors undergraduate course exams, research papers, and the Stacks Project. From each pool, 100 problems were formalized in Lean by five specialists who are all Mathlib contributors, including some working on the formalization of Fermat's Last Theorem, across five workshops of over five hours each. Two reviewers with mathematics and Lean expertise spent over 20 hours each checking the formalizations, with additional external validation from the Lean community.

Each Lean file follows strict standards: exactly one sorry after the final theorem, LaTeX natural-language descriptions as comments before formal statements, dependence only on Mathlib, self-contained files, and fixed universe levels.

For evaluation, the authors asked each model to generate a whole proof in a single pass, using pass@64 with a maximum token limit of 64k, and verified results with the Lean REPL through multi-process parallelization. Every proof was checked by the Lean kernel for sorry and compilation errors, and string-matching checks confirmed the theorem statements and definitions had not been modified. Separately, human mathematics experts graded the natural-language proofs generated by the models (pass@1), which allowed the authors to compare mathematical reasoning ability against formalization ability and to categorize the errors that occurred in between.

Why This Matters

Impact on research. The paper argues that verification is the bottleneck for using AI in frontier mathematics: natural-language proofs at advanced levels can only be checked by a small number of human experts, which is slow and unscalable. Formal verification through Lean is automated and reliable, but the results here show that current models cannot yet take advantage of it at research level. The finding that natural-language reasoning and formalization are largely decoupled, and that formalization is the weaker link, gives the field a concrete target.

• Automated proof checking for mathematical research. Formal verification pipelines could let mathematicians check complex proofs without long expert review cycles, though the paper shows existing LLMs fall far short of producing such proofs at research level.

• AI-assisted mathematical exploration. The FATE-X design expects models to discover phenomena, abstract them into lemmas, and formulate new definitions, which is what research-level mathematics actually requires, making the benchmark a gauge for tooling that could support working mathematicians.

• Formal library development. Because 38% of FATE-X requires definitions absent from Mathlib, progress on the benchmark would likely come with contributions to formal mathematical infrastructure such as local complete intersections and Gorenstein rings.

• Evaluation design for AI reasoning systems. The paper's two-stage evaluation (natural language first, then formalization) gives model developers a way to diagnose whether failures come from mathematical reasoning or from translation into precise language.

Industry relevance. The authors come from a mix of academic institutions (Westlake University, Peking University, Great Bay University) and industry (Ubi-quant), and the work is supported by the National Key R&D Program of China grant 2024YFA1014000, the New Cornerstone Investigator Program, and Ubiquant. The suggestion that retrieval-augmented generation over Mathlib could improve formalization connects directly to practical RAG and verification tooling, and the finding that specialized fine-tuning may degrade meta-reasoning ability is relevant to anyone training domain-specific reasoning models.

Future Directions

• Explicitly decoupled pipelines. The authors argue for separating the natural-language prover from a dedicated autoformalizer, rather than having one model perform both in a single pass, since the evidence suggests the stages are functionally decoupled.

• Training that preserves effective reflection. The paper raises whether DeepSeek-Prover-V2's lack of effective reflection is an unintended outcome of its specialized training scheme, and asks whether a training methodology can leverage precise formal reward signals while still fostering meta-reasoning capabilities such as effective reflection.

• Retrieval-augmented formalization. Because Mathlib hallucinations and Lean proficiency issues were the most common error types, the authors suggest a RAG system that retrieves relevant theorems from Mathlib and supplies accurate type information could improve formalization performance.

• Auxiliary lemma generation for new definitions. The case study found that models rarely generated auxiliary lemmas to help with problems involving new definitions, an ability the benchmark is explicitly designed to probe.

The authors also note that rigorously confirming these research directions is beyond the scope of the paper and remains a key task for future work.

Target Audience

This paper is most useful to AI researchers working on automated theorem proving and formal mathematics with LLMs, particularly those building or evaluating prover models in Lean. It also serves benchmark designers who need a graded, expert-curated evaluation beyond contest mathematics; mathematicians and Lean/Mathlib contributors interested in where formalization coverage currently ends; and ML practitioners studying how domain-specific training affects general reasoning and self-correction abilities. Readers need comfort with formal proof assistants and algebra to follow the benchmark content, though the high-level findings about the reasoning-versus-formalization gap are accessible to a broader machine learning audience.

Authors’ abstract

Recent advances in large language models (LLMs) have demonstrated impressive capabilities in formal theorem proving, particularly on contest-based mathematical benchmarks like the IMO. However, these contests do not reflect the depth, breadth, and abstraction of modern mathematical research. To bridge this gap, we introduce FATE (Formal Algebra Theorem Evaluation), a new benchmark series in formal algebra designed to chart a course toward advanced mathematical reasoning. We present two new components, FATE-H and FATE-X, each with 100 problems in abstract and commutative algebra. The FATE series spans a difficulty spectrum from undergraduate exercises to problems exceeding PhD qualifying exams. Notably, FATE-X is the first formal benchmark to surpass both PhD-level exam difficulty and the coverage of the Mathlib library. Our evaluations of state-of-the-art LLM provers on this new benchmark reveal a stark performance gap compared to contest math: the best model achieves only 3% (pass@64) accuracy on FATE-H and 0% on FATE-X. Our two-stage evaluation reveals that models' natural-language reasoning is notably more accurate than their ability to formalize this reasoning. We systematically classify the common errors that arise during this formalization process. Furthermore, a comparative study shows that a specialized prover can exhibit less effective reflection than general-purpose models, reducing its accuracy at the natural-language stage. We believe FATE provides a robust and challenging benchmark that establishes essential checkpoints on the path toward research-level formal mathematical reasoning.