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

TL;DR

FATE introduces a frontier formal algebra benchmark series (FATE-M, FATE-H, FATE-X) to evaluate AI-assisted formal mathematics at undergraduate to PhD-level difficulty. It documents a rigorous curation process, progressive difficulty, and formalization properties including new definitions in $FATE\text{-}X$ not yet in Mathlib, providing a challenging testbed for Lean-based formalization. Across extensive evaluations, state-of-the-art NL reasoning models show strong intermediate reasoning but fail to produce correct formal proofs, with top results at $3\%$ (pass@64) on $FATE\text{-}H$ and $0\%$ on $FATE\text{-}X$, highlighting a decoupled bottleneck in translation to formal language. The study advocates explicitly decoupling natural-language reasoning from formalization and emphasizes improving reflective reasoning to bridge the gap toward research-level formal mathematical reasoning.

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.

Figures (4)

• Figure 1: Main experimental results. (a) Formalization accuracy drops sharply along the difficulty progression of FATE-M, FATE-H ($\le$ 3%), and FATE-X (0%). (b) A significant gap exists between intermediate natural language reasoning and final formal proof generation. Model abbreviations: ds-r1 (DeepSeek-R1), ds-p-v2 (DeepSeek-Prover-V2).
• Figure 2: The curation process of FATE-H and FATE-X benchmarks
• Figure 3: Problem distributions by mathematical topics in FATE-H/X.
• Figure 4: Proof structure progression generated by DeepSeek-R1 on FATE-M, FATE-H, and FATE-X benchmarks. The colored segments represent different reasoning phases: initial theorem application (blue), synthesis of intermediate results (orange), and exploratory steps (green).