FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels
Authors: Jiedong Jiang
Wanyi He
Wang Yuefeng
Guoxiong Gao
Yongle Hu
Jingting Wang
Nailin Guan
Peihao Wu
Bryan Dai
Liang Xiao
Bin Dong
Venue: ICLR 2026 Poster (2026)
Keywords: Formal Theorem Proving
Benchmark
Mathematical Reasoning
Formalization
Algebra
Lean
Primary area: datasets and benchmarks

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**, 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.

Published as a conference paper at ICLR 2026
FATE: A FORMAL BENCHMARK SERIES FOR FRON- TIER ALGEBRA OF MULTIPLE DIFFICULTY LEVELS
Jiedong Jiang Wanyi He Yuefeng Wang?' Guoxiong G Yongle Hu
Jingting Wang? Nailin Guan? Peihao Wu Chunbo Dai Liang Xiao
Bin Dong*6tt
'Westlake Institute for Advanced Study, Westlake University PPeking University Ubi- quant "New Cornerstone Science Laboratory, School of Mathematical Sciences, Peking University Beejjig International Center for Mathematical Research and the New Cor- nerstone Science Laboratory, Peking University "Center for Machine Learning Research, Peking University "Center for Intelligent Computing, Great Bay Institute for Advanced Study, Great Bay University j jiangjiedong@eestlal wangj ingting223 mail inguan55))ssttu. pku. edu cn (phwu, 1xiao@bicmr pku. edu. en dongbin@math, pww..u..ccc....... edu.cn
(25011001,200110002, edu. on {2501110011, 2501110002, samggx huyongle, com
ABSTRACT
Recent advances in large language models (LLMs) have demonstrated im- pressive capabilitics formal theorem proving. particularly on contest- based mathemattcal benchmarks like the IMO. However, these contests do not reflect the depth, breadth, and abstraction of modern mathematical re- search. To bridge this gap, introduce FATE (Formal Algebra Theorem Evaluation U, a new benchmark series in formal algebra designed to chart course toward advanced mathematical reasoning. We present two new components, FATE-H and FATE-X, each with 100 problems 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 surpass both PhD--evel exam difficulty and the coverage of the Mathlib library. Our evaluations of stato-of-tho-art LLM provers on this new benchmark reveal stark per- formance 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. Fur- thermore, 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 the path toward research-level formal mathematical reasoning.
INTRODUCTION
The emergence of reasoning models (Guo et al. 2025: OpenAl, 2025; Authropic, 2025; Gem- ini Team, Google, 2025) has boosted the prospect that AI will assist in frontier mathematical rescarch and produce rigorous proofs. Although modern mathematics has been successfully built upon the foundation of natural language proofs, complex proofs generated by current models remain unreliable. A major obstacle improvement lies in verification: the more ad- vanced a natural language proof is, the more it relies on limited human experts for rigorous
"Equal contribution.
1 Corresponding authors.
'The FATE benchmark series is open sourced at httpp:///gittub..om///ee//////// /FaFEE /ATE. The evaluation code open sourced at http::///annbbccc///eeeynnntt/t.
1

---

Published as a conference paper at ICLR 2026
verification, resulting in a process that is slow, unscalable, and error-prone. This creates critical bottleneck for iterative dexelopment. In contrast, formal verification through proof assistants like Lean (Moura & Ullrich, 2021) provides an automated, scalable, and reliable alternative for proof checking (see Appendix A for an introduction).
Following this direction, the rescarch community has made rapid progress in formal anto mated theorem proninnrooinnn.oo with large language models (LLMs). State-of-tho-art sae-the-art-mddol- models RRen et al. 2025 Wang et al. 2025; Lin al 2025; Zhou et al, 2025: Chen et al., 2025) have achieved impressive results on existing benchmarks and even on IMO contests. However, current benchmarks have largely focused on two areas that differ significantly from modern mathematical research: contest-style problems (Zheng et al. 2022 Lin_et_tea_eeeee
moder
et al 2023 and introductory university-level mathematics (Azerbayev et al., 2022: Tsoukalas et al. 2024).
Mathematical contests often prioritize clever tricks over the systematic application of theoret- ical frameworks, and introductory university courses operate at a lower level of abstraction. In contrast, advanced mathematics is more open-ended, requiring not only the comprehen- sion and application of broad, deeply nested abstract concepts but also the exploration of new insights and the creation of Aheorelical frameworks. To address this gap, introduce two benchmarks: the graduate-level FATE-H (Formal Algebra Theorem (xvaluation-Hard) and the PhD qualifying leverieeeee FATE-X (-Expert) These benchmarks build upon the undergraduate-leve FATE-M benchmark by Shen et al, (2025) in the same domain, forming progressive series of increasing mathematical difficulty designed to assess formal reasoning from undergraduate to post-PhD qualifying examn levels.
FATE focuses on abstract and commutative algebra, a domain emphasizing abstract proofs and the study of structures, reflecting the character of modern mathematics. All problems were selected by expert mathematicians and formalized by specialists to ensure quality and originality. To our knowledge, FATE-X is the first formal benchmark whose mathematical difficulty exceeds that of PhD qualifying exams whose formalized content surpasses the current scope of Mathlib (mathlib Community, 2020). the mathematical library of Lean.
70%
Models
80%
Reasoning Models
Natural Language
80%-
o3
70%
Formal Language
ciaude-sonnet-4
gemini-2..5-pr
deepseck-r1
qwen3
50%
Theorem Provers
de-prover--22-777
40%
ximina-prover-722
goedel-
proeedl-prove--223325
30%
20%
20%-
12%
10%
0%
06
0%
0%
0%
0%
EXTE-M
RATE-II
FATE-X
da-p-v2
do-p-12
FATE-H
FATE-X
(a) Formalizaton accuracy (Pass064) across FATE-M/H/X benchmarks.
(b) Intermediate natural language (Pass@1) vs. formal language (Pass064) accuracy on FATE-H/X.
Figure 1: Main experimental results. (a) Formalization accuracy drops sharply along the difficulty progression of FATE-M, FATE-H (< 3%), and FATE-X (0%). (b) A significant gap exists between intermediate natural language reasoning and final formal proof generation. Model abbreviations: ds-r1 (DeepSeck-R1), ds-p-v2 (DeepScck-Prover:
To establish bascline performance, we conducted comprehensive, two-stage evaluation of state-of-the-art LLMs and specialized provers, mirroring their observed common process of first generating a natural language Chain-of-Thouglt (CoT)) and then formalizing it. We used expert human assessment for the CoT and automated verification for the final Lean code. This dual analysis revealed that formalization accuracy on research-oriented benchmarks is exceedingly low-withh top models achieving just 3% on FATE-H and 0% on FATE-X- a stark drop from their performance on contest-level problems. In contrast,
2

---

Published as a conference paper at ICLR 2026
the natural language reasoning was significantly more accurate, identifying the translation from informal reasoning to formal code as the primary bottleneck. Our case studies of this bottleneck showed that errors related to Mathlib hallucinations and Lean proficiency were the most common, while Misalignment issues were infrequent.
We also compare a general reasoning model (DeepSeck-R1) with specialized theorem prover SreepSekk-Prover--ee to analyze differences their reasoning behavior. Among our find- ings, PrepSeee--Pover--eee exhibits less effective reflection in natural language reasoning, resulting in siguificantly reduced accuracy at this stage.
To summarize, our core contributions are as follows:
1. Progressive Benchmark Creation. We introduce two new benchmarks, FATE-H and FATE-X (100 problems cach), and extend the existing FATE-M benchmark from 141 to 150 problems with quality improvements, forming the complete FATE series. This series spans from undergraduate to post-PhD qualifying exam level in algebra. To our best knowledge, FATE-X is the first formal benchmark to surpass PhD qualifying ezam diffieully and Mathläb's 's formalization coverage.
2. Baseline Performance Evaluation. We comprchensively evaluate state-of-tho-art models, establishing performance baselines where the best model achieves only 3% (pass@64) on FATE-H and 0% (pass@64) on FATE-X.
Natural and Formal Two-Stage Output Analysis. Based on the pattern of natural language reasoning followed by formalization in model outputs, conduct detailed two-stage analysis. Our evaluation reveals: (1) significantly higher accuracy in natural language reasoning versus formalization; (2) classification of common formalization er- rors: Mathlib hallucinations and Lean proficiency issues were the most common. General capability issues occurred with intermediate frequency, while misalignment were the least common; and (3) in comparative studies, that specialized provers exhibit less effective reflection in natural language reasoning than general-purpose models (DeepSeek-RI) resulting in reduced accuracy at this stage.
Sea-SeekkProoer--.
RELATED WORKS
Natural and Formal Mathematical Benchmarks Natural language benchmarks by Cobbe et al. (2021) and Hendrycks al. (2021) cover elementary to high school problems,
where leading model performance is nearing sa Sutrationn More-challengee
compet ptpppetiiioonn itn- based
benchmarks include those by He et al. (2024), Gao et al. (2025)__am) and Gulati et al (2024).
with progression to miversity and graduate levels in works by Sawada et al. (2023) Ean
al. (2025). Research- benchmarks by Zhang et al, Glazer et al. (2024), and partially Phan et al. (2025) represent the current frontier. common limitation of these benchmarks their reliance on final-answer verification.
al
(024) and Chernyshev
2025
Formal benchmarks enable reliable proof assessment. The miniF2F benchmark (Zhngg ct al 2022) focuses on mat hematiial competitions, with similar efforts including Liu et 22033 and Toonkllas et al. (2024). Universil
formalization inwiiiooonnnccueeee includes ProofNet (Azerbayev et al. 2022), hybrid datasets (Ren et al. 2025 Yu et al., 2025). specialized combinatorics
benchmarks (Xiong Baaonn_e__aall_ at 2023; Lin et al 2025), and the abstract algebra. benchmark
FATE-M (Shen et al. 2025). Hu et al. (2025) provides undergradiatt--ccosibbb problems
extracted from formal projects by supplying all necessary lemmas and defiiiiiion These are primarily implemented in Lean, building on Mathlib (mathlib Communiyy, 2020).
Formal Theorem Proving with Language Models Early systems by Polu & Sutskever
(2020) pioneered search-hased proof generation_ffllooeee followed by methooss.mmpooying variants of hest-first search (Yang et al., 2023; Lin et al. /01 Wt et al
2025: al. 2024: et
2025) and variants of Monte Carlo tree search (Lample et al., 2022 Gloockle et al 2024 Xin
et al. 2024). More More-recently, sotneeettssstttttffttteeee the-arr provers surcsssshhhas those by Ren et al. (2025): Lin
et al. (2025) ) Wang et al. (2025); Zhou et al. (2025); Chen et al. (2025) have shifted to single-
pass generation. Trained with large-scale reinforcement. learning, these models produce long
3

---

Published as a conference paper at ICLR 2026
chain-of-thoughh reasoning to decompose and correct Lean code, achieving accuracy rates approaching 100% on the miniF2F benchmark (Zheng et al. 2022).
3 THE FATE BENCHMARK SERIES: DESIGN AND CURATION
The FATE series consists of three benchmarks of increasing mathematical difficulty: FATE- M, FATE-H, and FATE-X. Among these, FATE-H and FATE-X are newly introduced, each containing 100 problems. The existing FATE-M has been expanded from 141 to 150 prob lems, with improved natural-languaee comments and formalization details while preserving the original mathematical content.
FATE focuses on abstract and commutative algebra, emphasizing proofs based on abstract properties and the study of algebraic structures instead of equation-solving or numerical computation, thereby reflecting the character of modern mathematics (see Appendix B.2.1 for common problem types). This area is particularly suitable for testing research-level rea- soning due to its abstract and self-contained nature, which enables deep problem-sol without requiring extensive mathematical input from other fields. Lean's 's existing algebra libraries provide solid foundation for research-level questions, enabling one to attack ad- vanced problems in this area with minimal additional formalization. Unlike benchmarks based on contest problems introductory undergraduate material, FATE is designed to es- tablish a difficulty progression toward modern mathematical rescarch, structured as follows:
FATE-M: Textbook- level basic exercises.
FATE-H:: Problems at the level of honors course exams or graduate-level difficulty.
FATE-X: Problems at the level of PhD qualifying exams or beyond.
This graded structure offers more comprehensive evaluation than a single accuracy score, preventing strong performance on simpler tasks from masking weaknesses in advanced rea- soning, or vice versa.
To demonstrate that the mathematical difficulty is progressive and reaching the PhD qual- ifying exam level, we first describe the curation process in Section 3.1 then focus on the mathematical content, followed by a description of formalization properties.) in Section 3.2 Representative examples from each benchmark are provided in Appendix B.1.
3.1 BENCHMARK CURATION
Data Sources Mathematical problems for FATE selected from established sources. The supplementary FATE-M problems are drawn from undergraduate textbooks. FATE-H and FATE-X problems spurced from: (1) more than 20 standard undergraduate and graduate textbooks, such as Lang (2012) and Eisenbud (2013); (2) publicly available PhD qualifying exams from various universities and exams for honors undergraduate courses; and (3) research papers and advanced community-driven resources such as the Stacks Project (Stacks Project Authors 2018).
Review
Collect
Formalize
Mathemetical Literature
200 + 200 Problems
100 + 100 Problems
(Natural Language)
(Formal Language)
Figure 2: The curation process of FATE-H and FATE-X benchmarks
4

---

Published as a conference paper at ICLR 2026
Curation Workflow The curation process for FATE-H and FATE-X is highly demanding, as it requires experts with deep mathematical knowledge, specialists in Lean formalization, and extremely rare individuals with dual expertise. Figure illustrates the curation process.
Collection: We collected and classified 400 candidate problems into two difficulty-bssed categories: FATE-H and FATE-X, cach containing 200 problems. The initial curation was conducted through a four-day collaborative effort involving nearly twenty postdocs and PhDs in pure algebra from top institutions, under the supervision of leading researchers. This process ensured the final selection is mathernttcaally profound, well-balanced across key topics, and challenging for both human and machine reasoning.
2. Formalization: A subset of 200 problems (100 from each category) was formalized in Lean by five experienced specialists, all contributors to Mathlib, Mathlii_including some involved in the ongoing formalization of Fermat's Last Theorem (Buzzard, 2024). This effort was organized into five dedicated workshops, each involving over five hours of collaboration.
The formalizations were checked and corrected by two reviewers with strong mathematical backgrounds and Lean expertise, each dedicating over 20 hours. Accuracy was further verified with assistance from external exports in the Lean community.
Review:
3.2 BENCHMARK CHARACTERISTICS
Problem distributions by mathematical topics in FATE-H and FATE-X are provided in Appendix B.2.2 and Figure The charts illustrate shift in focus from abstract algebra in FATE-H to advanced commutative algebra topics in FATE-X.
Progressive Difficulty Although a consensus exists among mathematicians regarding problem difficulty, it lacks objective measures. We support this from three aspects:
Case Studies We present three examples (one from each benchmark) in Appendix B.3.1 involving similar mathematical topics with increasing difficulty. Analysis shows that these problems require: (1) direct application of a theorem
linear deduction (FATE-M), (2) syuthetic analysis of several direct results as integrative reasoning (FATE-H), and (3) exploration and analysis of new mathematical objects after synthesis as recursive structural analysis (FATE-X). This forms a clear difficulty progression.
Human Performance Metrics We conducted a human experiment to quantitatively test the benchmark difficulty: Fach participant, either Ph.D. student or postdoc- toral researcher in algebra, was randomly assigned 5 non-overlapping natural language problems from FATE-H and FATE-X to solve in 2.5 hours. The participants achieved an accuracy of 73% on FATE-H and 21% on FATE-X, reflecting the significant difficulty progression across the benchmarks. The performance of LLMs also reflects a similar difficulty gradient, as detailed in Appendix B.3.2
Expert Assessment We conducted a questionnaire survey with ten professors from top institutions specializing in algebra (see Appendix B.4 for details). The results indicate that when comparing FATE to classical lextbooks and ProofNet, experts consistently rated FATE significantly higher in difficulty, coverage, and originality. Regarding the suitability of FATE problems for PhD qualifying exams, 7/10 experts indicated that the algebra qualifying
problems were either directly appropriate for Aegebra/commutee cxams notably more challenging than standard PhD qualifying exam questions.
Formalization Properties Due to its scope and difficulty, FATE-X uses mathematical definitions not yet present in Mathlib. In total, 38% of its problems require new definitions, which are formalized before the problem statement. This subset of problems averages 2.4 new definitions each. These include advanced concepts from commutative algebra, such as local complete intersections and Gorenstein rings. Consequently, LLMs must derive the necessary lemmas to use these definitions effectively. Morcover, to solve these challenging problems successfully, models expected to discover mathematical phenomena, abstract them into useful lemmas, and, when needed, spontaneously formulate new definitions. This capability is critical for research-level hematiila formalization and problem-solving.
5

---

Published as a conference paper at ICLR 2026
All benchmark problems follow strict formalization standards: each Lean file has only one sorry after the final theorem; natural language descriptions in [T]X are included as com- ments before formal statements; files depend only Mathlib and are self-contained; and universe levels are fixed to prevent issues from category theory.
4 EXPERIMENTS AND RESULTS
4.1 and 4.2 we detailed the experimental setup and baseline results on FATE. Observation of the model outputs indicated two-stage generation pattern, where natural language precedes formalization. Consequently, Sections 4.3 and 4.4 analyzo the impact of this two-stage process on the models' final accuracy separately. Section 4.5 presents comparalive study between a general reasoning model and a theorem prover. Finally, Section 4.6 provides comprehensive discussion synthesizing these findings.
In Sections
4.1 EXPERIMENT SETUP
Our experiment included general reasoning models such o3 OpenA 2025 Gemini-2.5
Pro Geminn Team Google. 2025), Blaude-4-Soune--hhing
(Anthropic, 2025) DeepSeek-
R1 Guo et al,, 2025) and Qwen3 (Yang al, 2025). We also tested state-ol-the-art theo- rem provers, including SpepSeek-Proveee V2-6711 (CoT), Kimina-Provee--2BB, and Goedel- Prover-7213 without self-correction mode. For both categories, we employed whole-proof generation, using pass064 metric (Chen et al 2021)
successful if at least one correct proof is found within 64 independent attempts with a maximum token limit of 64k. For detailed setup and prompt, Appendices F.1.1 and
During formal verification, we implemented multi-process parallelization using the Lean REPT (a read-eval-print-loon for Lean4) to enable efficient large-scale evaluations. Every proof is rigorously checked by the Lean kernel to confirm it contains no sorry or compilation errors. Furthermore, to ensure semantic correctness and prevent unintended modifications, we employ string- matihiigtthhnn checks to verify the accurate transcription of theorems and def- initions. Any gener-teee lemmas are also fillly compiled to confirm their validity. A detailed methodology is available in Appendix F.1.2.
4.2 BENCHMARR PERFORMANCE
Table 1: Formalization accuracy across FATE benchmarks (pass@64, max 64k tokens)
Model
FATE-M Reasoning model
FATE-H
FATE-X
o3
51.3%
3.0%
0.0%
Claude-Sonnet-l
45.3%
0.0%
0.0%
Gemini-2.5-Pro
40.0%
0.0%
0.0%
DeepSeek-RA
34.7%
0.0%
0.0%
16.0%
0.0%
0.0%
Theorem prover
DeepSeek--Prver--V2..
62.7%
3.0%
0.0%
Koedeel-Prover-V2-022
48.7%
2.0%
0.0%
36.0%
2.0%
0.0%
These results reveal a stark contrast in performance: while models achieve reasonable success rate on FATE-M, the best-performing model solves only out of 100 problemn FATE-H, and model produces any valid Lean proofs in FATE-X. Additional pass@2* results (for 0,1,...,66) 6) are provided in Appendix F.1.3

---

Published as a conference paper at ICLR 2026
To understand the reason behind low accuracy, examine the model's output and rea- soning content. We observed a consistent behavior across all models with visible reasoning process (DeepSeek-R1 and all theorem provers): els always first work out a full natural language (informal) proof, followed by formalizaion. Among those models without available reasoning content, Gemini-2.5-Par and Claude-4- sonnet-thinking also tried to solve the problem in natural language first in the output, while only o3 directly output formalization attempts without any natural language content.
without explicit instructions, mod-
Given the models' two-stage process (natural language reasoning followed by formalization), we investigate the impact of each stage on final proof correctness in the following two subsections. For a discussion of the interaction between these stages, see appendix C.1
4.3 NATURAL LANGUAGE REASONING ANALYSIS
In this section, we first present manual evaluation of the mathematical reasoning in the main experiment's output in Section 4.3.1. which reveals a significant. gap between the correctness of the natural language portion and the final formalization. Based this, argue that formalization ability is the primary factor in Section 4.3.3 To understand the gap between the intermediate result evaluated by and the model's real natural language mathematical ability, we also conduct an ablation study in Section 4.3.2
4.3.1 MANUAL EVALUATION OF NATURAL LANGUAGE PROOFS
The two-stage reasoning phenomenon observed in Section 4.2 prompted the models' final formalization failures stem from errors in their initial mathematical rea- soning, or from the translation process between natural language and formal language? To answer this, we organized a manual evaluation to independently assess the models' natural language reasoning abilities under the original task settings.
question: do
Our mathematics experts evaluated the pass@1 correctness of the natural language proofs generated by DeepSeek-R1, DoepSeek-Prover-V22 Kimina-Prover, and Goedel-Prover-V on FATE- and FATE-X. Manual evaluation criteria and procedures are detailed in Ap- pendix F.2. We attribute errors to four main categories: Gap, Hallucination, Reasoning Problem, and No Progression. See Appendix for dcfinition and examples. The overall results of the ovaluation are presented evaluation for some problems and found that the models do exhibit diverse behaviors the same problem; see Appendix for details.
Table g. Furthermore, we conducted a pass@ @6
Table 2: Comparing Natural Language (NL) (Pass@1) and Formal Language (FI.) (Pass064)
Proof Accuracy on FATE-H and FATE-X
FATE-H
FATE-X
Model
NL
FL
NL
FL
DeepSeek-R1
71.0%
0.0%
33.0%
0.0%
DeepSeck-Prover V2
39.0%
3.0%
9.0%
0.0%
Goedel-Provee V2
48.0%
2.0%
8.0%
0.0%
Kimina-Prover 35.0%
2.0%
3.0%
0.0%
4.3.2 ABLATION STUDY ON THE IMPACT OF PROMPTS
Before drawing our conclusions, must address potential confounding variable: does the formalization task itself suppress the model's natural language mathematical ability. Consequently, we designed an ablation study testing different prompt settings for DeepSeek- R1, see C.2. We find that the models' natural language mathematical ability is higher when unburdened by the prompt to generate formal proof. However, modifying the baseline prompt to explicitly require a "math-beeoro-lean output had almost no impact on accuracy regarding Reepscek-R1.
7

---

Published as a conference paper at ICLR 2026
4.3.3 ANALYSIS OF MAIN FINDINGS
Primary Bottleneck: The Translation to Formal Language. First, for all mod- els tested, intermediate natural language reasoning accuracy (pass@1) far exceeds final formalization accuracy (pass@64). The ablation study further suggests that the models' mathematical ability when tasked only with generating natural langnage proof provided with an informal statement is likely even higher than what this evaluation captured. In conjunction with our finding (see Section 4.4) that formalization attempts are highly aligned with their preceding natural language reasoning, these results together show that the bottleneck is not the mathematical ability itself. Rather, the critical challenge lies in the translation and implementation of a correct natural language proof into an absolutely precise formal language.
2. Difference in Mathematical Abilitics Between Models. At the level of natural language mathematical reasoning, the general-purpose reasoning model behave signifi- cantly better than the specialized prover models in Table 2. We will conduct deeper
comparative analysis of this phenomenon in Section 1.5
4.4 FORMALIZATION ERROR ANALYSIS
This subsection classifies and quantifies common LLM formalization errors. Our human Lean experts analyzed proof attempts from DeepSeck-Provers on DeepSeck-R1 on the FATE-H benchmark, selected for its significant gap between natural language and formal language accuracy. After natural language evaluation in Section 1.3.1. experts manually counted distinct formalization errors in mathematically correct but formally incorrect at- tempts. These errors fall into four categories:
1. Mathlib Hallucinations: Errors in this category involve the generation of non-existent or incorrectly used Lean theorems or definitions;
2. Lean Proficiency Issues: These are errors related to a lack of understanding of Lean's specific syntactic rules, sophisticated type system, or idiomatic proof structures;
3. General Capability Issues: This category includes problems such as modifying headers and the others -leaving sorrys, producing repetitive output unmatched brackets;
4. Misalignment: This error occurs when the model's formal proof is inconsistent with previous mathematical reasoning.
For more details of these four calegories, see Appendix D
Table 3: Formal error counting result. for models on FATE-H
Formal Error
DeepSeek- Prover- V2
DeepSeek-R1
Mathlib Hallucination
35/39
70/71
Lean Proficiency
36/39
70/71
General Capability (header)
63/71
General Capability (others)
19/39
18/71
Misaligument
3/39
0/71
For results in Table 1 the denominator is the number of whole proofs generated by LLMs, which intermediate natural proof is manually judged to be correct. Among the four errors, Mathlib hallucinations and Lean proficiency issues were the most common errors, frequently recurring within almost every single proof attempt. In contrast, misalignment were remark- ably infrequent. This suggests that Altrieval-augmennerr generation (RAG) system, which retrieves relevant theorems from Mathlib and provides accurate type information, could help improve formalization performance. As DeepSeck-Prover-V22 could not include its data for header-related issues. However, among other general pability issues, DeepSeek-Proot Proveek--rrv--Veee V2 performed notably worse. Additionally, we found that only DeepSeek- Provek-Prrve-- V2 exhibited repetitive proof steps and misalignment.
output lacks headers,
8

---

Published as a conference paper at ICLR 2026
A case study in Appendix D.2 revealed that the types of formalization errors FATE-X were consistent with those on FATE-H. Notably, for problems involving new definitions, models rarely generated auxiliary lemmas to aid in proving.
4.5 GENERAL MODELS VS. THEOREM PROVERS
As demonstrated by the experimental results in Section 1 the general-purpose reasoning model significantly outperforms the specialized proof-assistant model in terms natural language success rate. To investigate the root cause of this performance gap, we conducted a detailed qualitative analysis of the reasoning processes of DeepSeek- V3 (Liu et al,, 2024),, DeepSeek-Prowee V2, and DeepSeek-Rl-a series of models all post-trained from the same base model More detailed experimental setup, results and case studios are provided in Appendix Here, we summarize the main conclusions:
In the initial phase of reasoning, all three models often adopt similar strategies or invoke comparable concepts. However, as the reasoning deepens and established problen-solving patterns fail to address the specific problem, their behaviors diverge significantly. The typ- ical behavior for DeepSeek- V3 is to directly assemble associated concepts into a superficial argument. In contrast, both DeepSeek-Prover- V2 and DeepSeek-RI attempt to provide more detailed discussions.
The essential difference between the latter two lies in capability term effective flection: the ability to locate, diagnose and repair flaws. While DeepSeek-RA. can some- times achieve this, DeepSeek-Prover-VV as starting over or a rhetorical shift without a corresponding logical change. Furthermore, studying discovers non-aligned phenomena during mathematical reasoning unique to DeepSeek-Proveet V2. These behaviors, which also affect their performance, include ques- tioning the correctness of the problem statement itself after failure and even engaging in conscious cheating behaviors.
is confined to performing formal reflections, such
intermediate natural language accuracy results of three models in Table confirm these observations: the SeeoseeekProver-VVee which offers detail but lacks effective reflection, achieves a final success rate nearly identical to that of the formally reasoning DeepSeek- V3. Meanwhile, DeepSeek-R1, which possesses this capability, significantly outperforms both. Nevertheless, we must note that even DeepSeek-Re RRlss reasoning ability has its limitations when faced with truly complex reasoning environments.
The
4.6 IMPLICATIONS AND DISCUSSION
Our experimental results and analyses lead to two points for discussion regarding future rescarch in automated thcorem proving:
First, our findings show that whole proof generation models use two-stage process for formal proving: generating a natural language proof, then a well-aligned formalization, suggesting these stages are largely decoupled. Considering our findings that the intermediate natural language accuracy of waapnSeeee-PPoe---ee lower than pure natural language accuracy of DeepSeek-RI. Together, these points strongly suggest that an explicitly decoupled approach, developing a natural language prover and separate autoformalizer, would gain extra improvement.
lower than that of DeepSeek-Ri R1, further
Next, our comparative experiments reveal that the general-purpose model performs more "effective reflection", a capability crucial human mathematical reasoning. In contrast, the specialized prover, despite reinforcement learning in the narrower domain of formalization, did not gain the expected boost mathematical reasoning. Instead, its performance was often hindered by various misaligned behaviors that degraded its reasoning ability relative to the general model. Considering the comparison with its base model (DeepSeek- V3), this raises the question of whether the DeepSeek-Prover-VV V2's lack of effective reflection is an unintended outcome of its specialized training scheme. This, in turn, leads to a critical challenge for future work: is it possible to design a training methodology that can simultaneously leverage the precise reward signals from formalization while also fostering essential meta-reasoning capabilities such as "effective reflection"?
9

---

Published as a conference paper at ICLR 2026
Although our findings suggest these rescarch directions, rigorously confirming them is be- yond the scope of this article and remains a key task for future work.
5 CONCLUSIONS
To bridge the gap between contest-style mathematics and modern research, we introduced FATE-H and FATE-X, extending the FATE series of formal algebra benchmarks, which features a graded mathematical difficulty structure and a frontier research focus, Our eval- wation of state-of-the-art models reveals their significant limitations in conducting formal reasoning in advanced mathematics, with maximum pass rates of just 3% (Pass@64) on FATE-H and 0% FATE-X. Further analysis indicates that the primary bottleneck lies in the formalization stage, with errors stemming mainly from hallucinations of the formal library and insufficient language proficiency, rather than in natural language mathemati- cal reasoning, as the two stages exhibit a functional decoupling. Furthermore, we found that general-purposs reasoning models outperform their specialized counterparts, due to more effective "reflection" capability. These findings collectively point to two fundamental research directions: first, explicitly decoupling the task of natural language reasoning from formalization gencration; and second, balancing the pursuit of formal accuracy with the cultivation of effective and aligned reasoning capabilities.
ACKNOWLEDGMENTS
This work is supported in part by National Key R&D Program of China grant 2024YFA1014000, the New Cornerstone Investigator Program, and Ubiquant.
We wish to express our sincere appreciation Yutong Wang for generously providing the code for the Lean verification. We are deeply grateful to the following individuals for their contributions the selection mathematical problems for the FATE benchmarks: Kaiyi Chen, Haocheng Fan, Yiqin Hc, Yongle Hu, Shanxiao Huang, Yudong Liu, Tian Qiu, Yin- chong Song, Peihang Wu, Zhenhua Wu, Tianyi Xu, Zhchan Xu, Huanhuan Yu, Huishi Yu, Jiahong Yu, Zhanhao Yu and Xiao Yuan. We gratefully acknowledge the following individu- als for their careful assessment of natural language proofs and insightful feedback: Haocheng Fan, Haoda Li, Zhongjin Yan, Chaodong Yang, Yuji Yang, Shun Yin, Huanhuan Yu, Jiahong Yu and Weijun Yuan. We also thank Nailin Guan, Zixun Guo, Yongle Hu, and Jingting Wang for their dedicated work in formalizing mathematical problems. We extend sin- cere thanks to Johan Commelin and Christian Merten for their careful external review and corrections to the benchmark problems. We are also indebted Siddhartha Gadgil, Filippo A. E. Nuccio and Floris van Doorn for their valuable discussions and suggestions.
Finally, express our deepest appreciation the Lean community for developing and maintaining Mathlib Mathlib-withouu without this foundational infrastructure, this work would not be pos- sible.
REFERENCES
Anthropic. System card: Claude opus & claude sonnet. 4. Anthropic. May 2025. URL (ol00000500000001000044090000
https: /twp///wwww////cc anw.ropit 2a7c285. pdf.. Released May 23, 2025. Accessed on March 2026.
Jeremy Avigad, Leonardo De Moura, and Soonho Kong. Theorem proving in Lean. Carnegie Mellon University, 2021. URL https: httpppss//eaaapoveee.. github. io wtw.:/iitiooooem..oiiiii..
ng leann_
Zhangir Azerbayev, Bartosz Piotrowski, and Jeremy Avigad. ProofNet: A benchmark for
autoformalizing and formally proving undergraduate-leva mathematics problems. In Sec- ond MATH-AT Workshop, 2022.
Grzegorz Bancerek, Czeslaw Byliński, Adam Grabowski, Artur Kornilowiez, Roman Ma- tuszewski, Adam Naumowicz, Karol Pak, and Josef Urban. Mizar: State-of-the-ar and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker
10

---

Published as a conference paper at ICLR 2026
Sorge (eds.), Intelligent Computer Mathematics, pp. 261-279, Cham, 2015. Springer In- ternational Publishing. ISEN 378-3-319-20615-8, doi: 1978---319--0000 URL
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Dela- haye, Daniel de Rauglaudre, JlennCChrstorn Filliâtre, Eduardo Giménez, Hugo Herbelin, et al. The Coq proof assistant reference manual. INRIA, 1999.
Kevin Buzzard. The Fermat's 's Last Theorem Project. Blog Post, https://Leenprorte communii ty. gi thub.
2024.
Mario Carneiro. The type theory of Lean. Master's thesis Carnegie Mellon University, 2019. URL https: / thub. wwwccioo//iiiie http://wwww....ooo/oooooee//eeee d d/v1.0 wtt.0//main.......
Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xi- aoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, et al. Seed-prover: Deep and broad reasoning for automated theorem proving. Xix preprint wrXiv:2507.23722 2025.
Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde De Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. Eval- uating large language models trained on code. arXiv preprint ar NEF::2107.03374, 2021.
Konstantin Chernyshev, Vitaliy Polshkov, Vlad Stepanov, Alex Myasníkov, Ekaterina Arte- mova, Alexei Miasnikov, and Sergei Tilga. U-MATH: A university-level benchmark for evaluating mathematical skills in large language models. In Proceedings of the Fourth Workshop on Generation, Enaluation and Metrics (GEM), ), pp. 974-1001, 2025.
Karl Cobbe, Vineet. Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, al. Training verifiers to solve math word problems. arXiv preprint erXiv:2110.144 1416, 2021.
David Steven Dummit, Richard M Foote, et al. Abstract algebra, volume 3. Wiley Hoboken, 2004.
David Eisenbud. Commutative olgebra: with a view toward algebraic geometry, volume 150. Springer Science & Busincss Media, 2013.
Jingxuan Fan, Sarah Martinson, Erik Y. Wang, Kaylie Hausknecht, Jonah Brenner, Danxian Liu, Nianli Peng, Corey Wang, and Michael Brenner. HARDMATH: A benchmark dataset for challenging problems in applied mathematics. In The 4th Workshop on Mathematical Reasoning and AT at NeurIPS'24 24, 2024. URL https: http:///pppeee....eeeeese. wwwp:wwweee.....eeeeeeeeeeeeeeo poretfforu?? d=gt6pr[TEGL.
Bofei Gao, Feifan Song, Zhe Yang, Zefan Cai, Yibo Miao, Qingxiu Dong, Lei Li, Chenghao Ma, Liang Chen, Runxin Xu, Zhengyang Tang, Benyou Wang, Daoguang Zan, Shanghao- ran Quan, Ge Zhang, Lei Sha, Yichang Zhang, Xuancheng Ren, Tianyu Liu, and Baobao Chang. Omni-MATH: A universal olympiad level mathematic benchmark for large lan- guage models. In The Thirteenth International Conference on Learning Representations, 2025. URL
net fot.:/ooruullldyyyaafok
Gemini Team, Google. Gemini 2.5: Pushing the frontier with advanced reasoning, mul- timodality, long context, and next generation agentic capabilities. arXiv preprint ar arXix:2007.0000 06260, 2025.
Elliot Glazer, Ege Erdil, Tamay Besiroglu, Diego Chicharro, Evan Chen, Alex Gunning, Caroline Falkman Olsson, Jean-Stanislas Denain, Anson Ho, Emily de Oliveira Santos, et al. FrontierMath: A benchmark for evaluating advanced mathematical reasoning in AI. Xix preprint 2xXii:2411.04888 2024.
Fabian Gloeckle, Jannis Limperg, Gabriel Synnaeve, and Amaury Hayat. ABEL: Sample efficient online reinforcement learning for neural theorem proving. In The 4th Workshop on Mathematical Reasoning and Al ot NearIPS'24, 2024. URL https: /openreview _net/forrumiddkk3nnsjvvvt
11

---

Published as a conference paper at ICLR 2026
Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. Mizar in nutshell. Journal of Formalized Reasoning, 3(2):153-22) 245. 2010, ISSN 1972-5787. doi: 10. 10.6092 6092/issn.1972. 187/1980. URL https://ffr.unio..tttt www.u.iiiii...
Aryan Gulati, Brando Miranda, Eric Chen, Emily Xia, Kai Fronsdal, Brumo de Moraes Du- mont, and Sanmi Koyejo. Putnam-AXIOM: A functional and static benchmark for suring higher level mathematical reasoning, In The 4th Workshop on Mathematical Rea- soning and Al at NeurIPS'24, 24, 2024. URL https://openreviewwnnee. www.ne//foormmdde iom YXnwLZe0yf.
Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Peiyi Wang, Qihao Zhu, Runxin Xu, Ruoyu Zhang, Shirong Ma, Xiao Bi, et al. Deepscek-rl incentivizes reasoning in llms through reinforcement learning. Nature, 645(50881)663 638, 2025.
John Harrison. HOL Light: An overview. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (eds.), Theorem Proving in Higher Order Logics, pp. 60- 66, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. ISBN orgoog//ttt /10, 1007 0 10. /9978-9--612-0333----- 4. URL https: http://000..001.00.00000777----/ 59-9_4
doi:
org
Chaoqun He, Renjie Luo, Yuzhuo Bai, Shengding Hu, Zhen Thai, Junhao Shen, Jinyi Hu, Xu Han, Yujie Huang, Yuxiang Zhang, Jie Liu, Lei Qi, Zhiyuan Liu, and Maosong Sun. OlympiadBench: A challenging benchmark for promoting AGI with olympiad-leve) bilin- gual multimodal scientific problems. In Lun- Ku, Andre Martins, and Vivek Sriku- mar (eds.), Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Pupers), pp. 3828 3850, Bangkok, Thailand, August 2024. Association for Computational Linguisties. doi: 10. 18653 h1//////2222//// https://aclanthine logy. org /tgg/00244
/ acl-oo.co- URL
202222244202 20224..l2222... acl-lllnnnnnn 211/
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Mcasuring mathematical problem solving with the MATH dataset. In Thirly- fifth Conference on Neural Information Processing Systems Dalasels and Benchmorks Truck (Round 2), 2021. URL
net
(horum?id=7yytt2mmt
Jiewen Hu, Thomas Zhu, and Sean Welleck. miniCTX: Neural theorem proving with (long- ccontexts. In The Thirteenth International Conference on Learning Representations, 2025.
URL. /ttps://openreview.. httpiiiwwwwettteeee for.
Guillaume Lample, Timothee Lacroix, Marie-Amm Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. In Proceedings of the 36th International Conference on Neural Information Processing Systems, 2022.
Serge Lang. Algebra, volume 211. Springer Science & Business Media, 2012.
Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. Hun- yuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving. arXiv preprint ar Xiv: 10004222207333 2024.
Haohan Lin, Zhiqing Sun, Yiming Yang. and Scan Welleck. Lean-star: Learning to interlcave thinking and proving, 2024. URL https://arxiv org g abs /200 10040.
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yi- han Geng, Jiawei Ge, Jingruo Sun, et al. Goedee--rover--2: Scaling formal theorem prov- ing with scaffolded data synthesis and self-correction. ar preprinl ar Xrv:2250080000 03613, 2025.
Aixin Liu, Bei Feng, Bing Xue, Bingxuan Wang, Bochao Wu, Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, et al. Deepseek-v3 technical report. arXiv preprint arxiv:2412 19437, 2024.
12

---

Published as a conference paper at ICLR 2026
Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. FIMO: A challenge formal dataset for automated theorem proving. arXiv preprint arXiv:2309.00 04295, 2023.
Junqi Liu, Xiaohan Lin, Jonas Bayer, Yael Dillies, Weijie Jiang, Xiaodan Liang, Roman Soletskyi, Haiming Wang, Yunzhou Xie, Beibei Xiong, et al. CombiBench: Benchmarking Ilm capability for combinatorial mathematics. arXiv preprint orXiv:2505.03177 2025.
The mathlib Community, The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020.
Norman Megill and David A. Whoeler. Metomath: A Computer Language for Mathematical Proofs. Lulu Pross, 2019.
Leonardo de Moura and Sebastian Ulirich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Suteliffe (eds.), Automated Deduction CADE 28, pp. 625-635, Cham, 2021. Springer International Publishing. ISBN 978-3-030-79576-5
Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. Isabelle/ proof assislant for higher-order logic, volume 2283. Springer Science & Business Media, 2002. doi:
10.1007/3- 00077335500459999
OP Openai o3 and o4-mini system card. OpenAT, April 2025. URL https://open ai. com index -iniiii--iiiiiiie hnneer/ooooommmii---syste.arrr/ Released April 16, 2025. Accessed on March 8, 2026.
Long Phan, Alice Galti, Ziwen Han, Nathaniel Li, Josephina Hu, Hugh Zhang, Chen Bo Calvin Zhang, Mohamed Shaaban, John Ling, Sean Shi, et al. Humanity's 's last exam. Xin preprint orXi:225011142. 2025.
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprinl arXiv:2009.0333 2020.
ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu. Qihao Zhu, Dejian Yang, et al. SropSeck-Prover-Ve V2: Advancing for- mal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint 2ix::2504.21800 2025.
Tomohiro Sawada, Daniel Paleka, Alexander Havrilla, Pranav Tadepalli, Paula. Vidas, Alexander Kranias, John J Nay, Kshitij Gupta, and Aran Komatsuzaki. ARB: Advanced reasoning benchmark for large language models. arXiv preprint Sttt::2377.16992 2023.
Ziju Shen, Naohao Huang, Fanyi Yang, Yutong Wang, Guoxiong Gao, Tianyi Xu, Jiedong Jiang, Wanyi He, Pu Yang, Mengzhou Sun, et al. Real-prover: Retrieval augmented lean prover for mathematical reasoning. arXiv preprint arXiv:2505. 200,1, 2025.
Konrad Slind and Michael Norrish. brief overview of hol4. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar (eds.), Theorem Proving in Higher Order Logics, pp. 28 32, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. ISBN 975-3-540-71067777 doi: 10.1007 1---3--40---666- 6. URL /ttp::/s///oooooog/0000000000013 67-7_6.
The Stacks Project Authors. Stacks Project. https://stacks.mett wtw.ssaa.........ooooooom edu, 2018.
George Tsoukalas, Jasper Loe, John Jennings, Jimmy Xin, Michelle Ding, Michael Jen- nings, Amitayush Thakur, and Swarat Chaudhuri. PutnamBench: Evaluating neural theorem-provers on the putnam mathematical competition. In A. Globerson, L. Mackey, D. Belgrave, A. Fan, U. Paquet, J. Tomezak, and C. Zhang (eds.), Advances in Newral Information Processing Systems. volume 37. pp. 11545-11566, Curran Associates, Inc.. 2024. URL http:////o.pppecasseeeeeoo.oo/ar
T1135227ceccaaaaaaeeee000roppro0 ks_ ks_Track.pdff
13

---

Published as a conference paper at ICLR 2026
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos San- tos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Simina-prover pre- view: Towards large formal reasoning models with reinforcement learning. arXiv preprint ar X0v:20004 1 11354, 2025.
Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Zheng Yuan, Wenwei Zhang, Dahua Lin, and Kai Chen. InternLM2.5 s.repprore Advancing automated theorem prov- ing via critic-guided search. In 2nd AI for Math Workshop @ ICML 2025, 2025. URL
https: / http:////peeeeeeeeeeeeeeeeeeeeee eview.
Huajian Xin, Zz Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseel-prover--.. 5: Harnessing proof as- sistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint ar Xix:24408 08152, 2024.
Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Ming Ding. BFS-prover: Scalable best-first tree search for LLM-based automatic theorem proving. In Wanxiang Che, Joyce Nabende, Ekaterina Shutova, and Moham- mad Taher Pilehvar (eds.), Proceedings of the 63rd Annual Meeting of the Association for Computational Linguisties (Volume Long Papers), pp. 32588 32599, Vienna, Aus- tria, July 2025. Association for Computational Linguistics. ISBN 979-8-89116-251-44 doi: 10. 10.18653/ /v/ ong. 1565/
1565. URL https: wow.h//ooolattooooooooooooooo.o www.aannnoooooooo./2222......... a
Beibei Xiong, Hangyu Lv, Haojia Shan, Jianlin Wang, Zhengfeng Yang, and Lihong Zhi. A combinatorial identities benchmark for theorem proving via automated theorem genera- tion. arXiv preprint arXiv:2502.178 17840, 2025.
An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, et al. Qwen3 technical report. arXiv preprint Xrx: 09988, 2025.
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-angmented language models. In Proceedings of the 37th International Conference Neural Information Processing Systems, 2023.
Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, et al. FormalMath: Benchmarking formal mathematical reasoning of large language models. arXiv preprint TTw:2505.02793 2025.
Jie Zhang, Cezara Petrui, Kristina Nikolić, and Florian Tramèr. RealMath: A continuous benchmark for evaluating language models on research-level mathematics. arXiv preprint ar Xiv:2250 12575, 2025.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. MiniF2F: A cross-system bench- mark for formal olympiad-leve mathematics. In The Tenth International Conference on Learning Representations, 2022.
Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, Bohan Wang, Siran Wang, Luoxin Chen, Jiahui Wang, Haowei Chen, Allan Jie, Xinbo Zhang, et al. Solving formal math problems by decomposition and iterative reflection. aixiv preprint ar Xim:2200 15225, 2025.
14

---

Published as a conference paper at ICLR 2026
A INTRODUCTION TO FORMALIZATION AND LEAN
Mathematical Formalization Mathematical formalization is the process of translating intuitive, informal ideas and concepts into a precise, unambiguous language defined by strict logical rules. To support this process, interactive theorem provers (ITPs) assist users in constructing formal proofs. ITPs typically provide tactic mode, in which the prover tracks available hypotheses and the current goal as the proof state. Users manipulate this state through concise, high-level commands called tactics, and the prover automatically generates corresponding low-level proof code once all goals are solved. Tactics are designed to mirror patterns in natural language proofs, improving both readability and writability. Almost all L.M.-based formal theorem provers generate such tacties to construct formal proofs.
Varions ITPs built on distinct but equally sound logical foundations Metamath (Megil)
Wheeler, 2019) and Mizar (Bancerek et al. 2015; Grabowski, et 2010) are based on set Theory; HOL4 (Slind & Norrish,, 2008), HOL Light (Harrison 2009 and Isabelle/ HHOL HHOL NNipkow et 2002) are based on simple type theory; and Coq (Barras et al, 1999) and Lean MMura & Ullrich, 2021) are based on dependent type theory. The mathematical library available in each prover determines the difficulty of formalizing different topics. Lean's extensive and unified Mathlib (mathlib Community. 2020) distinguishes it from other ITPs.
Lean and Mathlib Lean (Moura Ullrich, 2021 is an interactive theorem prover based depeendentt type theory, with proof irrelevance and non-cumulative universes (Carneiro 2019). An introduction to the language can be found in (Avigad et al., 2021). Lean 4 is designed to be highly extensible through its metaprogramming capabilities, enabling the accurate and concise extraction of important metadata.
Mathlib4 (mathhib Community, 2020) is a community-driven effort to build a unified library of mathematics in Lean 4. It formalizes a substantial portion of modern mathematics and currently contains over 1,700,000 lines of code contributed by more than 550 developers. Mathlib covers a wide range of lopics, including algebraic geomelry, analysis, category the- ory, combinatorics, geometry, general algebra, linear algebra, logic, number theory, order theory, probability theory, and topology. Among these, the formalization in algebra is the most developed. This makes Lean particularly suitable for formalizing advanced mathemat- ies, especially in algebra. Such formalization remains inaccessible in many other interactive thcorem provers, which lack similarly extensive foundational librarics.
15

---

Published as a conference paper at ICLR 2026
B BENCHMARK QUALITY ANALYSIS
This appendix presents the quality of the FATE benchmarks, emphasizing their mathemat- ical content. Following illustrative examples from each benchmark in Appendix B provide case studies and statistics to demonstrate the diversity (see Appendix (.2) and progressive difficulty (sce Appendix B.30 of the problems. The results of an expert survey assessing the benchmarks are reported in Appendix B For comparison, examples from the FATE-M benchmark introduced by Shen al. (2025) are included. For analyses focused purely on mathematical content, we provide only the natural-lanuuaee problem statements without formalization details for brevity.
B.1 REPRESENTATIVE EXAMPLES
FATE-M
import Mathlib
/--
Suppose $D$ is integral domain, $m$ and $n$ are coprime positive integers. Prove that for any $a, b \in D$, if $a $ab and $a< we have $awb$.
-/
theorem
{R Type*} [Ring R] [IsDomain R] (a b R) (m n N) (hm : m 0) (hn 0) (hmn m. Coprrim n) (h: a m m) (h2 a
n) : =a= := by
sorry
FATE-H
import Mathlib
open IntermediateField RatFunc
/--
Let $\mathbb(F3344 the field with $4$ elements, $t$ transcendental over \mathbb(F3_4ss and $F #\mathbb(F3-A(tM4 t)$ and $K =\mathbb(FF-A4()). Show that $K$ is Galois over $F$.
theorem wtt.:/lisiieeeeaaaooooo.oooooooa
IsGalois (GaloisField (x 4 x RatFunc (GaloisField 2)))
(RatFunc (GaloisField 2)) := by
sorry
FATE-X
import Mathlib
/--
Let V( \) be domain and \) its field of fractions.
1( x Vin K \) is called almost integral if there exists an element
1( rlin A, \ne V) such that (( rxon \in \) for all \( n \ge \)
-/
def IsAlmostintegral {A Type} [CommRing A] [IsDomain A] (x FractionRing A)
Prop t= A, T T N, 3 A, (x n) algebraMap A (FractionRing A)
/--
1( A \) is called completely integrally closed if every almost integral element of \( K \) is contained in A( A V).
16

---

Published as a conference paper at ICLR 2026
-/ def I.sCopplttelyyinegralyyyooeddd (A : Type) [CommRing A] [IsDomain A] Prop :-
V FractionRing A, IsAlmostIntegral x A, x algebraMap A (FractionRing A)
/--
Let A(A \) be domain. Show that if V( V) is completely integrally closed, so is 1( A[X] A).
-/
theorem hwwp:/eeeyy..teerrl.....d....ooe
{A Type} [CommRing A] A)
[IsDomain A] (h ASCompeeteyynnterrallee
LsCompletelyynteerallyyy (Polynomial A) by
sorry
B.2 DIVERSITY
Appendix B.2.1 presents three principal problem types within the series, each accompanied by a representative case. The statistical distribution of mathematical domains is detailed in Appendix B.2.2
B.2.1 PROBLEM TYPES
The FATE benchmark includes variety of problem types, with three representative cate- gories outlined below.
Abstract Reasoning Problems These problems start from an abstract condition and require proving a general conclusion.
(FATE-M) Prove that if finite abelian group has order a power of a prime then the order of every element in the group is a power of p.
Concrete Example Problems These problems start from a specific, concrete example and ask for the proof of one of its properties.
(FATE-H) Prove that the order of Aut(Zs En) 108.
Open Constructive Problems These problems require the construction of an object that satisfies a specific property.
(FATE-X) There cxists two commutative rings R, S, such that R[x] is isomorphic to S[x] but R is not isomorphic to S.
The first. category, abstract reasoning problems, is the most common type in FATE-H and FATE-X. It is noteworthy that the abstractness of problem type does not directly correlate with its mathematical difficulty. A detailed case study on the benchmark's 's difficulty gradient available in Appendix B.3.
B.2.2 DOMAIN STATISTICS
We classify abstract algebra and commutative algebra into subfields and further break down these subfields into specific topics. For a complete list of subficlds, topics, and corresponding statistics, Table 4 for visual sunburst chart representation, refer to Figure 3. The chart illustrates a shift in emphasis from abstract algebra FATE-H to advanced commutative algebra topics in FATE-X.
17

---

Published as a conference paper at ICLR 2026
Table 4: Problem Distribution by Mathematical Topic in FATE-H and FATE-X
Subfield
Topic
FATE-H
FATE-X
Abstract Algebra
Basic Axioms and Examples
4
Subgroups and Quotient groups Group Actions and Sylow theorems
3
Group Theory
p-Groups, Nilpotent Groups and Solvable Groups
Basic Definitions and Examples PID, ED and UFD
Ring Theory
Polynomials
Field Extensions
Field Theory
Galois theory
11
11
Explicit Computations
11
Linear Algebra
3
Other Topics
Elementary Number Theory
1
Commutative Algebra
Ideals and Modules Localization and Decomposition of Ideals Integral Dependence and the Nullstellensatz Noetherian rings and Chain Conditions Dedekind Domains and DVRs Tensor Product and Flatness
5
3
7
Ideal Theory
4
2
Heights and Dimensions
2
Dimension Theory and Smoothness
Regular Sequences and Regular Local Rings Smoothness and the Module of Differentials Depth, Cohen-Macaulay Rings and Gorenstein Rings
4
0
Completions and Hensel's lemma Algebraic Number Theory and Valuation Theory Algebraic and Arithmetic Dynamics
Other Topics
Homological Methods
0
Noncommutative Algebras
0
B.3 PROCRESSIVE DIFFICULTY
Appendix B.3.1 presents three topic-related examples of increasing difficulty, demonstrat- ing the progressive structure of the benchmarks. Furthermore, Appendix [B3.2 provides statistics on model output token length and natural language accuracy to reflect problem difficulty.
B.3.1 CASE STUDY: GRADED CHALLENGE ON NON-SIMPLE GROUPS
To demonstrate the difficulty gradient of the FATE benchmark, analyze the solutions and reasoning contexts generated by DeepSgek-R1 on three topic-related problems from FATE-M, H, and X. As illustrated in Figure 4. the model's generated proofs exhibit a clear progression in structure and complexity, reflecting the increasing mathematical difficulty of the problems.
For the M-level problem, the approach is direct: the model applies Sylow's theorem to single prime p (as suggested by the problem setup) and reaches the conclusion directly using the given conditions. In contrast, for the H-level problem, the single- approach is insuf- ficient. The model synthesizes information from Sylow's theorem applied to all prime factors of the group order and employs counting argument to derive contradiction. The X-level problem requires an additional step: after performing the aforementioned analyses, several possibilities remain. To resolve these, must examine new objects and conduct further
18

---

Published as a conference paper at ICLR 2026
Adelli and Modoles
and Byow thepeemn
Genig Actione
Rinm Theory
Dedekinn ploppine and Pryite
idkal Theory
Commutatiiv Algebra
Croup
Abstrrcc
Aggebaa
retk weds
Other Topios
Oene Toplcs
Alai Haaryy Samaie
Expiet Computations
Tneory
Liber
Fioid E Exbrnttons
Gotoil theery
FATE-H
Ideall and Movtubos
Grocp Actione and Parovenn
2001
ming Theory
Group mioor
Ldea Theory
aigh and
Abstrnct
Fod Thuorr
Algebon
Commutativn
Golois theory
Alpebri
Tensor Product Platnamo
Other Topics
Dimonsion Theary and Smmotimnee
Noights and Dimansions
(b) FATE-X
Figure 3: Problem distributions by mathematical topics in FATE-H/X.
19

---

Published as a conference paper at ICLR 2026
analysis using Sylow's theorem Aheorem--ppecffcallly specifically, by investigating the relationship between the normalizer of the Sylow 17-subgroups and the Sylow 3-subgroups.
FATE-M
FATE-H
FATE-X
be finite group of order p"q. where and primes with Then Sylow p-subgroup of normal. (As
Prove that #G 56 then & not simple.
Prove that
simple.
consequence, not simple.)
Approach
consider Sylow 7-subgroups,
Sylow subgroups
1. "Syyoo'' Third Thearen"::
<..> By Sylow's third theoren:
for the primes 3,5,7,27.
<..pplly sylow for p=7.,>
<.applyy sylow for every possible
Analysis*";
Now consider the sylow 2-subgroups.
Thus:
c.apply sylow for p=2.>
n_3 (7,85,595)
Contradiccioo for V(np q
left with n_7=8 and n_2-7. <.>
Thersfore,
(21,51)
(.>
n_7 (15,85)
leading to contradiction.
n_17 (35)
48 elements order 7,
5.>
the renaiiing 56-48-8 elerents nust
So total nonidentity elenents of
forn the Sylow 2-subgraup?
prine order: 2 4 6tn7 568
wait, we have Sylou
subgroups, each of order B. How can only elenents left? <.>>
<.long reasoning about counting.>>
But
find contradiction the remsining cases.
Thus, is not simple.
<.>>
specific combination. For example, combination 1: n3=7, n7-15.
<..log exploration.>>
But Sylox 3-subgroup that is nornalized
give subgroup generated by and that sylou 3-subgroup, which would orden 17*3-51. subgroups of order 51. (This is the critic construction)
know
are
c..long reasoning, failed at the end..>
Figure 4: Proof structure progression generated by DeepSeek-RI 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).
From Proof Structure Capability Gradient The increasing complexity of the required proof structure is directly reflected in the model's output. The reasoning content produced by the model aligns with this structural progression, as visualized Figure using distinet colors to mark different reasoning stages:
The M-level problem exhibits a simple sequential dependency chain, requiring only linear deduction. Its monolithic, unidirectional reasoning is represented by single blue block:
The H-level problem requires a tree-like dependency structure. The model's initial paral- lel explorations (blue block) converge into a final synthetic conclusion (orange block) process we term integrative reasoning:
The X-level problem corresponds to a more complex, nested proof structure. After initial analysis proves insufficient, one must extract a new mathematical object from the proof state and reapply major theorems it (green block). This nested re-analysis of intermediate results requires recursive structural analysis.
In summary, the difficulty gradient in this case arises from the deliberate design of increas- ingly complex proof structures, which in turn demand progression of capabilities: from linear to integrative to recursive structural reasoning.
B.3.2 AUXILIARY STATISTICS ON PROOF DIPFICULTY
In this section, we present two statistics: (1) human evaluation of the intermediate natural language accuracy during the formalization process of DeepSeek-R1 FATE-M, FATE-H,
20

---

Published as a conference paper at ICLR 2026
and FATE-X; and (2) the average output token length of various reasoning models when solving natural language mathematical problems without formalization.
As noted at the end of Section 1.2. the model first prosuces complete natural language solution before formalizing it. The data in Table reflect expert evaluations of these in- termediate natural language solutions (Pass@1), showing clear decreasing accuracy trend from FATE-M to FATE-H to FATE-X.
Table 5: Intermediate Natural Language Accuracy Across FATE-M/H,
Model
FATE-M
FATE-H
FATE-X
DoepSeck-R1
94.7%
71.0%
33.0%
should be noted that these results do not directly represent natural language performance, since the model's final task is formalization rather than natural language proof generation. An ablation study in Appendix C.2 compares natural language accuracy between direct natural language task and the intermediate natural language output within the formalization task. The results show that although pure natural language task yields higher accuracy, the improvement is significantly smaller than the gap between different levels and therefore does not affect the observed decreasing accuracy trend across the three benchmarks.
Table Average Output Token Length on FATE-M/H/X (Pass@1)
Model
FATE-M
FATE-H
FATE-X
o3
1122.4
3799.5
6203.5
Claude-Sonnet-4
3827.8
11872.2
12118.8
Comini-2.5-PPa
4867.5
8508.6
14694.1
DeepSeek-He R1
3845.0
10625.1
16597.4
The token length data in Table 8 indicate a clear incrcasing trend output token length from FATE-M to FATE-H to FATE-X across all models.
B.4 EXPERT ASSESSMENT
We distributed questionnaire 10 professors specializing in algebra and number theory at top institutions, consisting of two parts: (1) comparison of the difficulty of FATE against a classical textbook and the ProofNet (Azerbayev et al,, 2022) benchmark, and (2) assessment of the suitability of FATE benchmark problems for use in PhD qualifying examinations.
In the parst.part, we divided the FATE-H and FATE-X benchmarks, classical algebra text- books (Dummit et al. 2004), and the algebra component of ProofNet by mathematical topic. We then randomly sampled 10 problems with balanced topic distribution from each to form three anonymous problem sets. Participants were asked to compare and select the best set across several dimensions. The results summarized as follows:
For the most difficult, 10/10 choose FATE.
For the best coverage, 8/10 choose FATE, 2/10 choose hard to distinguish.
For the best test deep understanding, 9/10 choose FATE, 1/10 choose classical text- book.
For the most original, 9/10 choose FATE, 1/10 choose hard to distinguish.
For the best evaluate ability in mathematical research, 9/1 /010 choose FATE, 1/10 choose classical textbook.
has shown that an absolute majority experts support the view that the problem set chosen from FATE has the best difficulty, coverage, ability to test deep understanding,
21

---

Published as a conference paper at ICLR 2026
originality, and effectiveness for evaluating ability in mathematical research, compared to the problem sets chosen from classical textbook and ProofNet.
In the second part, randomly sampled an additional 30 non-overlapping problems from FATE-X while maintaining balanced topic distributions. Minor supplements from FATE-H used to adjust the proportion of abstract algebra and commutative algebra. Partici- pants were then asked to evaluate the suitability these problems for PhD qualifying cxams based on several criteria. The results are summarized follows:
For coverage of knowledge points in PhD qualifying exams, 4/10 choose completely cov- ered, 2/10 choose almost completely covered, 3/10 choose mostly covered with no impor- tant points omitted, 1/10 choose important points omitted.
For difficulty; 7/10 choose meets exceeds PhD qualifying exam level, 3/10 choose meets excellent undergrad uate level.
For ability to differentiate students, 3/10 choose very well, 1/10 choose reasonably well, 3/10 choose insufficient.
For possibility to construct PhD qualifying exam, 4/10 choose possible, 6/10 choose need adjustment. Among those choosing need adjustment, 3/6 report too difficult, 3/6 report need more topics like group representation theory.
The results show that absolute majority recognize that the problem set meets exceeds PhD qualifying exam difficulty and mostly covers knowledge points in abstract and com- mutative algebra with no important points omitted. One important factor affecting both differentiation ability and exam construction is that the problem set is more difficult than standard PhD qualifying exams.
C ANALYSIS OF NATURAL LANGUAGE OUTPUT
C.1 INTERACTION BETWEEN NATURAL LANGUAGE REASONING AND FORMALIZATION
In the main body of this paper, we conclude that the natural language mathematical rea- soning stage and the formalization stage are functionally decoupled in current models. This appendix serves to explore the few, yet insightful, cases where a positive interaction between these two stages does occur.
clear example this interaction is when the formalization process reveals mathemat- ical error in the preceding natural language proof: In the following example, the model DeepSeck-RR initially derived an incorrect formula for an element count. was only when attempting to formallze this flawed formula that the model recognized its logical mistake and reverted to the natural language stage to correct it.
Output of DeepSeek-R1 (FATE-X)
totalLeleeentts_acccuutee = 1 + 2n_3 + 4n_5 6n_7 560. // The model initially provides counting formula, but forgets to include elements of composite order.
let .lements.prime__oxers
:= (Finset.univ.filter (fun x
p, p.Prime ^ orderOf p)).
But note: we are counting elements of prime order?
// During formalization, it reflects on the true meaning of the equation.
<...>
So the total number of elements is:
1 [n3*2 n5#4 n7*6 n17+16] composite order elements) 1785.
// It then corrects the counting formula to include all elements.
22

---

Published as a conference paper at ICLR 2026
The comments after // in the code block explain the model's behavior.
In addition to this, a similar interaction observed when a model deems a mathematically valid natural language proof to be ill-suited for formalization. In such instances, the model may also abandon its initial natural language proof and return to the reasoning stage to devise alternative strategy that is more amenable to formalization.
Paradoxically, this consistent pattern of interaction reinforces the hypothesis of functional decoupling. Whether the feedback from the formal language stage reveals mathematical error or a practical formalizalion obstacle, the model's response is the same: reverts to the natural language stage to perform the core logical revision. The model does not fix the mathematical logic within the formal framework; instead, it treats the formal language stage verifier that sends the task back to functionally separate natural language "prover". This workflow highlights a clear separation of concerns, further supporting the view that decoupled, two-stage rescarch approach is a promising path forward.
C.2 ABLATION STUDY OF PROMPTS
To understand how the prompt influence the model's natural language performance, we designed pass@1 abldtion testing four different prompt settings for DeepSeek-R1 FATE-X, see Appendix G.2 for explicit prompts:
1. Baseline Prompt: Requires generating a Lean proof and provides the formal statement.
2. Pure Math Prompt: Does not require generating Lean and does not provide the formal statement.
3. Math Output Prompt: Does not require generating Lean but provides the formal statement.
4. Math-before-Lean Output Prompt: Builds on the Baseline Prompt, adding a clear instruction to "output the mathematical proof first".
Table Natural language accuracy of DoepSock-RI under different prompts on FATE-X
Baseline
Pure Math
Math Output
Math-before-Leau Output
Accuracy
33%
43%
39%
32%
The results, shown in Table reveal the following:
The primary influencing factor is the formalization task itself: When the model's objective includes generating Lean code (comparing Prompt 1 and 3), the correctness of its natural language reasoning significantly decreases.
A minor factor is the formal context: When the model is shown the formal state-
ment (comparing Prompt 2 and 3), the correctness of its mathematical reasoning slightly decreases.
Explicitly requiring math-first output has almost no effect: The results for the Explicit Instruction Prompt 4 were nearly identical to those for the Baseline Prompt 1.
C.3 CASE STUDY: COMMON ERRORS IN NATURAL LANGUAGE REASONING
To better understand the models' weaknesses in reasoning, we analyzed and categorized errors in their natural language proofs. These categories are not non-overlapping classi- fication but a summary of typical failure modes observed by our experts that covers most issues. Since advanced models often make subtle errors, this classification relies not just the raw output, but also on an expert's deep understanding of the problem and experience grading.
23

---

Published as a conference paper at ICLR 2026
C.3.1 GAP
Gap occurs when the model's reasoning direction is correct but leaves key, non-trivial step not proved. This often involves secretly assuming necessary lemma or citing an overly powerful theorem bypass the argument.
Natural Language Problem Statement
(FATE-X) Prove that if #G 396 then G is not simple.
Model Output (DeepSeek-Prover-V))
If $n_2 99$, count elements:
$99 \cdot 297$ elements of order $2$ $4$.
Total elements $\geq 120 176 297 593 396$, contradiction.
Analysis standard solution here is to derive a contradiction by counting elements in all Sylow subgroups. However, crucial premise for this method is the proof that any two distinct Sylow subgroups have trivial intersection. DeepSock-Prover- skips this key argument, which is itself difficult and key part of the problem.
C.3.2 HALLUCINATION
A Hallucination is explicit statement of a false mathematical fact, typically stemming from an incorrect recollection of theorem or flawed mathematical intuition.
Natural Language Problem Statement
(FATE-X) Let. k be field, and set A Show that A is Gorenstein.
y2, ",,2-,,,,,,2,,,,
Model Output (DeepSeek-R1)
For Artinian local ring to be Gorenstein, it suffices to show that the socle (Seeratorname(Soc(()) \operatorname(Socc(() 1. <..>
has \dim_k
Analysis This is a factual error; the condition that the socle has dimension is not sufficient to be Gorenstein (the correction need an extra condition). Notably, all tested results (including DeepSeek-Prover-VVe V2, DeepSeek-R1 in attempts) made the exact same mistake this problem, suggesting common knowledge gap in current models regarding more specialized algebraic theory.
C.3.3 No PROGRESSION
model cxhibits "No Progression" when it fails provide any substantive mathematical progress, for instance, by reformulating the problem oi-similar to "Gap" error-citin an overly powerful theorem. The crucial difference is that a "Gap" involves some substantive progress, while "No Progression" does not.
(FATE-X) Let K K/Q be finite extension. Let y be a nontrivial element of the absolute Galois group G(K) of K. Show that admits an infinite number of conjugates.
Model Output (DeepSeek-RI)
24

---

Published as a conference paper at ICLR 2026
<... step 6: the center of the absolute Galois group of a number field is trivial. This is theorem. <...
Analysis The "theorem" stated by the model is, in fact, equivalent to the original problem The problem's actual difficulty lies in constructing specific field extensions. The model thus mercly restated the problem. It is worth mentioning that in the pass@16 experiment for this problem, almost all attempts made no progress. This outcome suggests a view also supported by our expert evaluators that problems eliciting "No Progression" response lap into a fundamental mathematical difficulty that is particularly useful for differentiating the capabilities of tate-offthhearr art models.
C.3.4 REASONING PROBLEM
Unlike the previous three categories, which relate primarily to mathematical knowledge or strategy, a Reasoning Problem stems from deficiencies in the model's general-purpos reasoning capabilities. Here, the model uses largely correct mathematical facts but con- neets them with flawed logical flow. Because the patterns these crrors are more complex, we provide detailed discussion and case analysis in Appendix b
C.4 VARIANCE IN NATURAL LANGUAGE REASONING
In our pass@16 16 evaluation of the following problem in FATE-X, we found that the model initiated three proof routes that are fundamentally different in their mathematical essence. worth noting that while the model made errors the latter exccution of the two non-standard routes, expert mathematicians confirmed that all three discovered approaches correspond to viable proof strategies.
PROBLEM STATEMENT
(FATE-X) Let be a prime number. Let K/Q be finite extension, such that the p²-th rool of unily contained in K. Let L/ be a Galois extension of degree p. Show that there exists Galois extension L' L'/L of degree p, such that the extension Z//K is also Galois.
The model's approaches are summarized below:
Method (Attempt 1) This is the most common and standard approach, directly applying Kummer theory for construction:
<...> XAPA2 a' over K' <...>
Method (Attempt 3) This more abstract, existential proof that also applics Kummer theory but relies on an extra deep property of number fields' multiplicative group:
the key point is: in a number field, the group K^*((A#) Ap is infinite.
Method 3 (Attempt 12)
This is a seemingly direct shorteut that bypasses the general thcory: the construction of the cyclotomic field extension.
To get a nontrivial element, we can take the class of T_p^2 in <...>
On this open-ended constructive problem, the model was not limited to a single solution but independently explored and initiated three valid paths of varying difficulty and abstraction.
25

---

Published as a conference paper at ICLR 2026
Its strategic distribution also aligns with human intuition: the most standard approach (Method 1) appeared most frequently. This performance also indicates that a model's ability to discover diverse proof strategies deeper mathematical capability-can be effectively tested even when its executional precision remains imperfect.
D ANALYSIS OF FORMAL LANGUAGE OUTPUT
This appendix provides an in-depth characterization of the four formalization error cate- gories identified in Section 4.4. accompanied by illustrative case studies.
D.1 DETAILED FORMAL ERRORS
Mathlib Hallucinations Errors in this calegory arise when models generate references to theorems in Mathlib library that do not exist or are used incorrectly the given context.
Hallucinating Theorems or Instances: Models may attempt use or make up theorems, definitions, typeclass instances which does not exist in Mathlib is named differently,
Incorrect Naming Conventions: Models might incorrectly guess the name of an existing Mathlib lemma or definition, resulting in unknown identifier error.
3. Misundorstanding of Conclusion Forms: Models may incorrectly predict the exact form, argument order, or return type of a Mathlib function or theorem (e.g., applying a lemma whose output type does not match the current goal).
Lean Proficiency Issues This category encompasses errors related to the model's in- complete or incorrect understanding of Lean's 's specific features, conventions, and design principles, beyond simple syntax.
1. Familiarity with Lean Design and Formal Disciplines: Models struggle with Lean's unique design choices. This can include difficulties with specific constructs such as knowing when a specific instance must be available for a tactic work, or understanding the implications of open inappropriate namespace leading to name conflicts.
2. Pure Syntactic and Type-related Problems: include incorrectly using structure dot notation, attempting to тW a let binding (which not directly rewritable), or failing to explicitly specify lype annotations where Lean's type inference struggles.
Minor but critical syntactic errors. Examples
3. Incorrect Prediction of Non-Finishing Tactic Outcomes: Models often fail correctly predict whether a non-finishing tactic will successfully make progress towards the goal or simply fail. For instance, while (rewrite) tactic sometimes be predicted, the outcomes of complex simp (simplification) tactics are highly unpredictable without inter- active exccution.
General Capability Issues This category encompasses fundamental problems related to the model's ability to follow instructions or maintain coherence.
1. Instruction Following Failures: Models generate erroneous import statements modify the given formal statement, even when the prompt. explicitly forbids such alterations.
2. Collapsing Repetition: Models sometimes fall into repetitive loops, generating the same sequence tactics or proof pattern multiple times, or producing long stretches of text that do not advance the proof. This indicates failure in coherent generation or inability to terminate a thought process.
3. Leaving sorry placeholders: The model fails to complete parts of the proof, leaving sorry placcholders which indicate an admitted gap in the formal argument.
Mismatching Parentheses/ baaessee/Brackttss /Brackets: Basic syntax errors, such as mismatched parentheses, square brackets, curly braces, lead to compilation failures.
26

---

Published as a conference paper at ICLR 2026
Misalignment This error occurs when the model's formal proof is inconsistent with pre- vious mathematical reasoning.
We now present partial formal proof generated by Deepseek-Proves V2 that covers the first three types of errors.
Failed General Capability Issues: Instruction Following Failures (header) import Mathlib. GroupTheory www.yyrrooouooooooo www.uucctio...uuuppppp import Mathlib.GroupTTee Index <..>
open Subgroup QuotientGroup Function Cardinal
noncomputable theorem
{G Type} [Group G] {n N} (hn # 0) (H Subgroup G) (hH H.index n) Subgroup 6,
K.Normal K H K.index
K. K.index n. factoriia by
Failed by Mathlib Hallucinations: Misunderstanding Conclusion Forms
haveI Fintype (G H) #..intyyequotieenoFiinneeeeed (by rw [hH]; exact
nat_lt_alephl n)
have card_quot Fintype.card (G H) by
rw
at hH
Failed by Lean Proficiency Issues: Familiarity with Lean Design exact hH let v Equiv.Perm / H) := MulAction. toPermHom / H)
let G / Fin := sttiippeeeuuiFinfCCarraa card_quot Failed by Lean Proficiency Issues: Fami Familiarity with Lean Design Let G Equiv.Perm (Fin n) : (MulAction. toPermHom G (Fin l
(MonoidHom.com comp PErui congr symm) q)
Let Subgroup G := MonoidHom.ker v
-- Failed by Mathlib Hallucinations: Incorrect Naming Conventions have K_normal Normal = ammoidHom..er_nonmee V
have K_le_H : K s H := by
intro g hg
change V
at hg
Failed by Lean Proficiency Issues: Pure Syntactic and Type-related Problems
have v by TW [hg, map_on, one_apply]
<..>
For the other two general capability issues, repetition and leaving sorry,we selected example illustrate.
Repetition case from Deepseek-Prover-vv <...>
have hr Fintype.card (Sylow G) [MOD 3] by
have ha Fintype.card (Sylow 3 G) = [MOD 3] := by
have he Fintype.card (Sylow low 3
[MOD 3] by
have haS : Fact Prime 3) t= hg
have hµ Fintype.card (Sylow 3 G) [MOD 3]
exact? exact h
exact hg
exact ha
'sorry' case from Deepseek-Prover-V2
intro
TW [dist_eq_norm, dist_eq_norm, one_mul]
sorry Continuity of the linear map
27

---

Published as a conference paper at ICLR 2026
SOrTy Injectivity
Sorty -- Surjectivity
Here is example for misalignment from Chepseek-Prover-- V2. During the formalization process, the model abandoned the correct method of mathematical reasoning in the step of proving that an(x/180) is algebraic and instead used mathematically incorrect path.
Problem Statement (FATE-H)
Prove that sin 1 is algebraic over Q.
Model Output (Deepscek-Prover-V2
<..>
The complex number (e={i=/180)' is root of unity (specifically, '360'
root unity, since (e={ix/t10)))((60) e^[i2x] = 1').
-The sine can be expressed as "sin(r/180) = (e^{ir/180} e4{-im/180))
which is a polynomial expression 'e<{in/180}' and its algebraic
conjugates.
The field of algebraic numbers is closed under addition, multiplication, and taking roots, so "sin(x/180)* is algebraic.
theorem isAlgebraic..in.pi.ddv
IsAlgebraic Q (sin (rr / 180)) := by have h_main 3 (p Polynomial Q), p # Polynomial.aeval (sin (x 180)) = 0 := by ma matmmtticaa incorrect step
have h IsIntegral @ (sin (r 180)) : by
have ha IsIntegral R (sin (= 180)) by
apply isintegraLLalgebaakg
exact
IsIntegral.of-finiz Q R (sin (s / 180))
have h IsAlgebraic Q (sin (= 180)) := h, isAlgebraic
D.2 CASE STUDY FATE-X
We conducted case study on FATE-X, observing that the categories of formalization errors made by the models were consistent with those identified in FATE-H. Given the novel for- malization fcatures of FATE-X, we specially examed the models' behavior on these problems with new definitions.
Due to the structured output tendency of Deepseek- Deepseek-Prover-V. V2, we focused our analysis solely on Deepseek-R11 results. We observed that the model seldom generates new lemmas re- lated to the general mathematical properties of the problem's 's definitions definitions beyond abbreviations. Furthermore, in no example did the model attempt to establish lemmas concerning novel mathematical properties presented in the problem state- ment. This suggests that models do not typically prove reusable theorems (i.e., connections between abstract properties) generate such lemmas even when defining new objects.
establishes new
In the example below, we highlight the new definitions and lemmas output by the model. Deepseek-R1 established a mathematical object already present in the problem statement. Tn subsequent lemmas, the model attempted to prove basic properties of this object. However, it failed to establish any Jemmas concerning the new mathematical properties introduced in the problem statement.
definition, but this merely served
abbreviation for
28

---

Published as a conference paper at ICLR 2026
##*# New definitions lemmas generated by Deepseek-R1
namespace GorensteinProof
variable (k Type) [Field k]
new definition
def MvPolynomial (Fin 3) k span (f(x 0)^ 2 -(x 1)^2, (X 1)^2 (x
2), (x 0) (x 1), (x 1) (x 2), (x 2) (X 0)3 Set (MvPolynomial (Fin
3) k))
variable {k}
instance CommRing (A k) <..>
instance Algebra k (A k) <..>
instance Module.Finite k (A k) <..>
instance FiniteDimensional (A k) Module.Finite. fimiiiteeiiittteiimssioooaaa
Lemma fielduo_ (h: (LocalRingg.axxmmalaa maximalldeal (A k)) IIMaxiimal) RocalRing.ResiideFiell.. (A k) =** := by <..>
lemma isLocalRing IsLocalRing (A k) := by <..>
Lemma isArtinian IsArtinianRing (A k) :=
<...>
E COMPARATIVE ANALYSIS: GENERAL MODELS VS. THEOREM PROVERS
comparison of intermediate natural language accuracy on FATE-H (Table 3 reveals that DeepSeek-R1 significantly outperforms both DeepSeck-V? V3 and Proverrr.. The latter two models exhibit similar performance.
Table 8: Intermediate natural language accuracy of DeepSeek-V3, DeepSeek-Prover V2, and DeepSeek-RI on the FATE-H benchmark.
DeepSeek-V3 V3
DeepSeek-Prover--22
DeepSeek-RI
Accuracy
40 %
39 %
71 %
In this section, asterisk (*) indicates that the results for this model were not obtained from our main experiment.
E.1 ANALYSIS OF BEHAVIORS DURING REASONING PROCESS
In research-level mathematical reasoning, the initial phase often requires associating the concepts in a problem with common proof patterns or established theories to guide the exploration. This phase primarily tests prior knowledge and mathematical intuition. We observe that the three models in the DecpSock series often exhibit similar approaches, and occasionally fall into the same traps, during this stage.
CASE 1: SIMILAR INITIAL INTUITION (FATE-H)
Problem Statement
29

---

'izeta' to Published as a conference paper at ICLR 2026
Let be the splitting field of
-- f(x)
2 - x + +
+
x
x²
++
@. Let C be of f()), i.e., a primitive seventh root of 1. Let ( c2 +5 Show that the intermediate field ((3) is actually Q(v-7).
Model Output DDeppSeek-Prover-V2
key observation:
The element 'lbeta = \zeta \zeta^2 \zeta<4* sum
terms that are permuted by the Galois group of \f(x)* over "mmatbbb()''. The Galois group isomorphic to (\matthbb22///maatbbbbb (aathbb/23/6\mathbbb/22
\cong
**Deriving the Minimal Polynomial of >**:.....
Model Output (DeepScek-R1)
--Let 'ttau \sigma~{23', So the subgroup 'H \/mathrm(idd, \tau, \tau"2)3* has order 3... Now observe that \bbet = \zeta \zeta^2 + \zeta74* is fixed by '\tau'
<..>
Model Output (DeepSeck-V3)
'Ibeta' is fixed by the Galois automorphism 'zetaa2"'
'/sigma' sending
(This is cited from its formal proof, because the output provides very few natural language reasoning.)
Analysis: In Case all three models first considered the Galois action on the cyclotomic field, as it is the most relevant systematic theory. However, the most direct solution to this problem does not require such background knowledge, as evidenced by DeepSeck-Prove Prover- V2's subsequent adoption of an independent proof strategy.
As reasoning deepens, established theories templates often provide only framework or, more weakly, a mere directional hint. The core task then becomes filling in details, adjusting the approach, and iterating through trial and error. This process, which demands deep thinking and what we term effective reflection the ability to locate, diagnose, evaluate, and repair internal flaws in argument-is crucial.
At this stage, DeepSeek- V3 typically resorts to skipping the details within the framework fabricating intermediate conclusions. Lacking robust reflective capability, DeepSeek- V3 often fails to deeply analyze or simply sidesteps the problem's 's core challenge.
CASE 2: SIDESTEPPING THE CORE CHALLENGE (FATE-H)
Problem Statement
Let R be an integral domain and let i,j be relatively prime integers. Prove that the ideal (x* v²) a prime ideal R[x,y]
Model Output (DeepSeek-V3)
30

---

Published as a conference paper at ICLR 2026
step3, We show that ((xi y*j\) is irreducible by using the fact that \XXi Y*j\) is irreducible in \R[X, when A(i) and A(j)) are coprime (this is a known result from algebra). <...
Translating the problem of proving prime ideal to proving the irreducibility of its generator is a standard method in commutative algebra. The main challonge of this problem, however, lies in proving this irreducibility. DeepSeek-V3 V3 cireumvents this task by citing it as a "known result".
Analysis:
In contrast, while DeepSeek-Prowee Prover-Vo V2 engages in more detailed reasoning, it often fails to properly evaluate, summarize, or correct its attempts. Instead, tends to abruptly switch to a new line of reasoning or introduce different errors, which hinders its ability to construct effective long-chain arguments.
CASE 3: INEFFECTIVE -LLLEAVAUATION (FATE-H)
Problem Statement
Prove that #G = 56 then G is not simple.
Model Output (DeepSeek-Proverr-Ve
<..>
The remaining 8 elements must form the Sylow 2-subgroup, <..
These 8 elements must be the unique Sylow 2-subgroup.
<...>
However, the most straightforward way is to use the following logic: <...>
But this is still not correct: <...>
The correct way is observe that if n2=7, then G acts transitively these subgroups
<..>
A better way is to use the counting argument:
<..>
Analysis: PaasSeck-Prove--222 behavior here is highly typical. It begins with a correct counting-bascd approach but then abruptly shifts a slightly diffcrent counting argument. It subsequently retracts this, moves to group action approach (failing to notice counting error within it), and finally returns its initial argument. This demonst that DeepSeek- Prover-V2s V2's "reflection" is often formalistic exercise in changing direction rather than a substantive self-assessment. The disconnectedness of the reasoning across paragraphs indicates inability to effectively evaluate its own arguments.
DeepSeek-R1, however, sometimes demonstrates ability to make minor but effective ad- justments to its reasoning path. It can extract useful information from incomplete lines of argument and occasionally exhibits iterative error correction (Case 4). Yet, this very iterative process rapidly increases the complexity of the reasoning stale, posing signifi- cant challenge the model's putext-handllng capabilities. In such complex environments, DeepSeek- R1 is still prone to reasoning errors (Case 5).
CASE 4: ITERATIVE CORRECTION (FATE-X)
Problem Statement
Let A R|x, (1/(X2+ +1). Then is a principal ideal domain.
31

---

Published as a conference paper at ICLR 2026
Model Output (DeepSeek-R1*)
<..>
So what the ideal that we should consider? <..>
Therefore, the ideal generated by x Y <... No, because = (2x+2y) <..> For example, the point (i,0) is defined over the complexes <...> we cannot write it as (x - i, Y) because not in the base ring. <..> So (x, Y-1) has common zero, by Hilbert's Nullstellensatz, it is the unit ideal?
<..>
This excerpt shows DeepSeek-RI attempting to construct non-trivial ideal. It tries define an ideal by picking points in the complex field but realizes through several attempts that these constructions are either invalid or lead to the trivial ideal. Through this process trial and error, it gradually recognizes that a non-trivial ideal must be constructed over the reals and correctly connects the problem to the conditions of Hilbert's Nullstellensatz.
Analysis:
CASE 5: FAILURE IN COMPLEX REASONING STATE (FATE-X)
Problem Statement
Prove that if #G 1785 then G is not simple.
Model Output (DeepSeek-R1)
<...> Combination n3=7, n5=21, n7=15 2*7=14, 4*21=84, 6+15=90; tota-=14+84+90-168 $\leq$ 1224 -> ok, but then C-1224-188-1056-0, so no contradiction.
So only combinations 1-8 are possible. Let's take a specific combination. For example, combination 1: n3=7, n5=21, n7=15.<..> The normalizer has index n3=7, so its order is 1785/7=255.... But we can't get a contradiction from that.
<..>
the number of Sylow 17-subgroups: n\_17 in the normalizer: must divide 255.
This solution is also discussed in the most difficult example of Appendix B.3. 1 As the analysis before, after applying sylow theorem and counting elements, the model reduces the problem to eight possible combinations of Sylow subgroup counts. It then explores a specific case (Combination 1) and derives intermediate result-that the normalizer of a Sylow 3-subgroup has order
A Analysis:
this path does not lead to a contradiction. The model then returns to the general case and successfully deduces a key relationship between the Sylow 17-subgroups and Sylow 3-subgroups. Unfortunately, it then incorrectly applies the intermediate result (order 255), which is valid only for Combination 1, to the general argument, causing the proof to fail.
We note that on the more difficult FATE-X problems, the performance gap between DeepSeek-RI and DeepSeck-Provet P2 widens even further than on FATE-H. This suggests that for frontier-level mathematics, the guidance offered by prior knowledge and established patterns becomes increasingly insufficient. Instead, the ability to conduct long-range reason- ing within complex state and, crucially, to loacate, diagnose and repair flaws via effective reflection. becomes the determining factor. We therefore believe that enhancing the capac- ity for deep thinking with effective reflection, demonstrated by general reasoning models, a more promising path toward research-leved mathematical Al than merely expanding model's repository of prior knowledge.
32

---

Published as a conference paper at ICLR 2026
E.2 MISALIGNED BEHAVIORS IN NATURAL LANGUAGE REASONING PROCESS
In addition to differences in reasoning ability, we observed behaviors in DeepSeck-Proot Prover-Ve V2 model that inconsistent with the core objective of solving the mathematical problem.
CASE 6: CONSCIOUS "CHEATING" (FATE-H)
Problem Statement
Let Dg be the dihedral group with 8 elements. Prove that Aut(Ds) Ds.
Model Output (DecsSce-PProve--22
<..>
'theorem problem_59 Nonempty (MulAut (DihedralGroup 4) DihedralGrouu 4) by classical apply Nonempty.intre sorry' The simplest. This is admittedly cheating, but it matches the requirements of the Lean problem.
<..>
Analysis: In this case, the model explicitly acknowledges that it is "cheating" by using sorry bypass the proof and satisfy the formal verifier.
CASE 7: QUESTIONING THE PROBLEM STATEMENT (FATE-X)
Problem Statement
Let be a Noetherian ring, C Q prime ideals such that == h, ht htQ d, where d > 1. Prove that there exist infinitely many intermediate primes P', P C P C Q such
that ht P' = + and ht Q/P'
Model Output (DeepSeck-Prover-V2
Wait, no: Lean, 'Ideal.height' the Krull dimension of 'R / ('I.height krullDim (R I)'), not the height of 'I' commonly defined in commutative algebra! But 'krullDim (R / Q) d by assumption, so 'd 1', which is false for 'd > 1'. This is contradiction unless the interpretation is incorrect.
Analysis: After a period of standard reasoning, DeepSeek-Provers arrives al a contra- diction due to a misunderstanding the formal definition of hdeght in Lean. Instead of questioning its own interpretation of the formal library, it concludes that the problem statement itself must be flawed.
F EXPERIMENT DETAILS
In Appendix F.1. we detailed our formal experiment setup, encompassing both the genera- tion and verification phases, while Appendix F.2 further claborates on the process, standards, and methodology for our manual natural language evaluations.
F.1 DETAILED BASELINE EXPERIMENT SETUP
F.1.1 GENERATION
For main experiments, deployed all theorem provers services with OpenAI-style API interfaces. Similar to the general reasoning models, we interacted with these large models via API calls. In all experiments, consistently used maximum token length of
33

---

Published as a conference paper at ICLR 2026
64k. The temperature settings were kept their defaults for each model: OpenAI models defaulted to a temperature 1 (ranging from to 2), while both Gemini and Authropic models defaulted to 1 (ranging from 0 to 1).
F.1.2 VERIFICATION
This appendix explained the verification methodology in Section 4.1 employed to ensure the correctness and integrity of the generated Lean proofs, especially considering the models' flexibility to generate auxiliary definitions and lemmas.
The verification process is divided into string checking and Lean REPL testing.
String-Based Pre-validatinn Initially, we perform series of string-based checks the generated Lean code. This involves removing all comments and using based rogular expressions based Lean keyword to identify all headers (including import, namespace, section, and other configurations), definition, instance, lemma, and theorem stalements. After standardixing import stalements to import Mathlib, proceed with several string- level validations:
1. Keyword Detection: We scan for critical keywords such as axiom, opaque, unsafe, or unsound. The presence of any such keyword immediately flags the proof as failure;
2. Component Alignment: We verify that all definition, instance, and lemma statements from the original problem's 's formalization exactly appear in the extracted components of the generated formal proof, and critically, that they appear in the correct order. Any deviation in sequence or omission leads to the proof being marked as failure;
Theorem Statement Match: final structural check ensures that the theorem component extracted from the generated file preciscly matches the main theorem statement of the original problem. Any mismatch also results the proof being deemed a failure.
Lean Verification Upon successfully passing all the string- based checks, every formal proof is rigorously checked by the Lean kernel to confirm it contains no sorry compilation errors. For our experiments, we used different Mathlib versions for each benchmark to align with the state of the library at the time of their creation. Specifically, the evaluations for FATE-M, H, and FATE-X were conducted using Mathlib versions 4.13.0, 4.16.0, and 4.19.0, respectively. We set a timeout of 300 seconds and use the preloaded Mathlib cache.
A proof that passes both phases is considered to be correct.
F.1.3 ADDITIONAL PASS@K RESULTS
We report @ass@k results (with h = 2 for 0,....6) 6) in Table for the FATE-M and FATE-H benchmarks, omitting FATE-X as no model achieved successful proof. These results are estimated from 64 samples per problem using the unbiased estimator:
Pass@k
Eproblems
as introduced in Chen et al. (2021).
F.1.4 PERFORMANCE UNDER NORMALIZED BUDGET
We report model accuracy using Pass0k under a normalized computational budget. As the input (the question statement) is significantly shorter than the output, we approximate the total cost by model size x average output tokens x number of samples. The results under this normalized budget are shown in Table 10. Closed-source models are excluded due to their undisclosed model sizes, and FATE-X is omitted as all recorded values were
34

---

Published as a conference paper at ICLR 2026
Table 9: Pass@k results across the FATE series.
(a) Pass@k FATE-M (%).
Passük
Model
4
16
32
Reasoning model
03
24.8
32.3
38.7
43.
46.2
48.8
51.3
Claude-Sonnets
11.6
16.7
22.6
29.0
35.2
40.6
45.3
Gemini-2.5-PM
8.0
12.3
17.4
23.0
28.7
34.4
40.0
DeepSeck- R11
7.4
11.3
15.8
20.4
24.8
29.3
34.7
Qwen3
2.7
4.3
6.2
8.5
11.0
13.6
16.0
Theorem Prover
Seepseek-Provee V2-671B
25.3
33.7
41.0
47.2
53.2
58.8
62.7
Goedel- Provee-Prover-eee V2-32B
21.2
26.9
32.3
36.9
41.0
44.9
48.7
Kimina- Kimina-Prover-P75
10.5
14.5
19.0
23.8
28.4
32.5
36.0
(b) Pass0k on FATE-H (%).
Pass@k
Model
2
4
8
16
32
64
Reasoning model
o3
0.1
0.2
0.4
0.8
1.4
2.2
3.0
Hlaude-Soneet.l
0.0
0.0
0.0
0.0
0.0
0.0
0.0
Gemini-2.55PP
0.0
0.0
0.0
0.0
0.0
0.0
0.0
DeepSeek-RR
0.0
0.0
0.0
0.0
0.0
0.0
0.0
Qwen3
0.0
0.0
0.0
0.0
0.0
0.0
Theorem Prover
Deepseek-Provers Propeek--Proee---2--6BBBB V2-671B
0.4
0.7
1.1
1.7
2.2
2.5
3.0
Goodel-Prover V2-32B
0.4
0.7
1.1
1.5
1.8
2.0
2.0
0.5
0.8
1.1
1.3
1.6
1.9
2.0
F.2 NATURAL LANGUAGE ACCURACY EVALUATION
F.2.1 EVALUATOR QUALIFICATIONS
To ensure a professional and accurate evaluation, we convened a leam of mathematical experts. All evaluators are PhDs postdoctoral researcher in algebra with deep domain expertise. Furthermore, all have prior experience grading university-level mathematics ex- aminations as teaching assistants or examiners, making them well-versod the standards of academic proofs.
F.2.2 EVALUATION WORKFLOW AND STANDARDS
Our evaluation workflow was designed to assess the validity of model-generated natural language proofs in an objective and consistent manner.
Understanding the Ground-Truthe Proof Before reviewing any model output, evalu- ators were required to first carefully read and fully understand the ground-truth proof of the problem, grasping its key steps and core idcas.
Assessing the Model's Proof Based their understanding of the ground-truth proof, evaluators then judged whether the natural language text generated by the model consti- tuted valid mathematical proof. Given that this evaluation aims assess mathematical
35

---

Published as a conference paper at ICLR 2026
Table 10: Formal accuracy comparison under normalized sampling budget across the FATE scries.
(a) Normalized Accuracy on FATE-M.
Model
Size
Avg. Length
Pass
Accuracy (%)
Reasoning model
Deepseek-R1 Qwen3
671B
10700
2
11.3
235B
11700
5
6.9
Thcorem Prover
Deepscek- Prokee--Poe--ee- V2
671B
4600
4
41.0
Goedel-Proven V2
32B
6300
64
48.7
Moinina-Prover
72B
12000
15
28.0
(b)
Normalized Accuracy FATE-H.
Model
Size
Avg.
Length
Pass
Accuracy (%)
Reasoning model
Deepseek-R1
671B
17300
1
0.0
Qwen3
235B
17500
3
0.0
Theorem Prover
Prepsock-Provert V2
671B
11400
2
0.7
Goedel- Proniel--Prve---e
32B
13700
30
2.0
72B
21000
9
1.4
ability in a decoupled manner, evaluators were instructed to completely disregard any for- malization code and its associated errors, focusing solely the mathematical logic of the natural language portion. It is important to note that judging the "validity" of a natural language proof inevitably relies on the professional knowledge and subjective judgment of the evaluator, which underscores the importance of our evaluators' expert background.
Standard for Adjudicating Long Outputs We observed that reasoning models, such as DeepSeck-R1, often produce exceptionally long outputs containing extensive preliminary thoughts, trials, self-corrections, and even discarded paths. For this scenario, we established a clear standard:
The evaluator's primary task is to locate and identify the proof that the model ultimately presents as its "final answer".
Using this "final proof" as a thread, the evaluator must then trace back and integrate all relevant arguments that the model provided throughout its entire reasoning process to support this conclusion. Components of the argument are sometimes scattered across the long-form output.
The final judgment is based on this reconstructed, complete chain of reasoning.
F.3 JUDGMENT AND ATTRIBUTION
Based on the above standards, evaluators provided a conclusion and attribution for each model output.
Validity Assessment:
First, to determine if the reconstructed proof was valid and whether there were any logical gaps, particularly in its core steps.
Error Attribution: If the model failed to provide correct proof, the evaluator was required to clearly identify the core error and provide a reason. This provided crucial data for our subsequent error analysis.
36

---

Published as a conference paper at ICLR 2026
Evaluator Remarks; After completing the above tasks, encouraged evaluators to write down any additional observations or comments on the model's performance. These remarks provided valuable qualitative insights into the models' "thought pat- terns".
G PROMPTS
G.1 MAIN EXPERIMENT PROMPTS
For theorem provers that provide prompt in the original paper, we the specified prompt, which is listed below. For other models, we employ the following bascline prompt:
Bascline Prompt
You are an expert in Lean and Mathematics. Please finish the following proof in Lean4 code. Do not change the original statement. Copy the final statement to prove exactly. Please include the complete header (including imports namespaces) that your code can pass the Lean4 compiler. Please solve the statement step by step and provide your complete Lean4 code between ">lean and after careful reasoning. The statement for you to complete is:
"Llean4 [FORMAL_STATEMENT]
PrepSeek-Prover--2((CTTT Goedel Prompt
Complete the following Lean code: ">lean4 {FORMAL.STATEMENT?
...
Before producing the Lean code to formally prove the given theorem, provide detailed proof plan outlining the main proof steps and strategies. The plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof.
Kimina Prompt
Think about and solve the following problem step by step in Lean 4.
# Problem: | [INFORRMLLSSTTTEMMNTT
# Formal statement:
**leaa
{FORMAL_STATEMENT]
..
G.2 NATURAL LANGUAGE ABLATION
Pure Math Prompt
You are an expert mathematician the field abstract algebra and commutative algebra. Your task is to provide complete and detailed proof for the following mathematical problem. The solution will be meticulously assessed by human expert for correctness, clarity, and logical rigor. So while you can assume foundational knowledge, every step of your argument must be explicit, rigorous, and logically sound. Prob lem:
(INFORMAL.STATEMENNT]
37

---

Published as a conference paper at ICLR 2026
Math Output Prompt
You are expert in Mathematics. Please complete the following proof. The problem stated in Lean4 code. You don't need write formal -proofall reasoning and proofs should be explained in natural language. Solve the statement step by step and provide your final answer after ###Final Answer, after careful reasoning. The statement for you to complete is:
"Llennd (FORMAL_STATEMENT]
Math-before-Lean Output Prompt
You aтe an expert in Lean and Mathematics. Please finish the following proof in Lean4 code. Do not change the original statement. Copy the final statement to prove exactly. Please include the complete header (including imports and namespaces) that your code can pass the Lean4 compiler. Please solve the statement step by step and provide your complete Lean4 code between "eeand and after careful reasoning. Please also write down your complete natural language proof in detail before the Lean4 code. The statement for you to comples lomplete is:
"Llann {FORMAL_STATEMENT]
...
H USAGE OF LLM
During the preparation of this manuscript, large language models were used solely for the purpose of language polishing.
38


Reviews:
[{"review_id": "EPdpO43spe", "reviewer": "Reviewer_fbC3", "summary": "This paper introduces FATE, a benchmark suite designed to evaluate the frontier of automated formal theorem proving in algebra. It extends previous work (FATE-M) with two new datasets: FATE-H, representing graduate-level difficulty, and FATE-X, targeting or exceeding PhD qualifying-exam level. Each contains 100 formalized problems in abstract and commutative algebra, curated and verified by experts using Lean. The authors evaluate a range of state-of-the-art LLM provers, finding drastic performance drops from FATE-M to FATE-H and FATE-X. Through a two-stage analysis, they show that the main bottleneck lies not in mathematical reasoning per se, but in translating correct natural-language proofs into formal Lean code. They further classify common formalization errors and compare specialized vs. general reasoning models, highlighting that general models exhibit stronger “reflection” capabilities.", "questions": "1. The paper mentions that abstract and commutative algebra is suitable for testing research-level reasoning due to its abstract and self-contained nature. Could the authors elaborate on whether they considered other fields for a frontier benchmark (e.g., topology, functional analysis) and what made algebra uniquely suitable as the first domain to push past the PhD-level frontier?\n2. In Table 2, the natural language (NL) accuracy is only reported for DeepSeek-R1 and DeepSeek-Prover-V219. Given the compelling finding regarding \"effective reflection\" (Section 4.5), obtaining NL accuracy for Goedel-Prover-V2-32B or Kimina-Prover-72B would be highly valuable to generalize the claim about specialized provers. Could the authors confirm whether these models also generate an explicit natural language proof (or Chain-of-Thought) that could be manually evaluated, and if so, provide those additional data points in the final version?\n3. Have you measured approximate human success rates or time to solve for graduate students or PhD candidates? This would ground the “difficulty” claim quantitatively.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 2, "strengths": "Originality: The paper fills a major gap between contest-level and research-level mathematical benchmarks. The design of a progressive benchmark series is conceptually novel and important for longitudinal evaluation of reasoning systems. The detailed error taxonomy (Mathlib hallucination, Lean proficiency, misalignment, etc.) provides a structured lens for analyzing formalization failures.\nQuality: The benchmark construction is rigorous: problems collected, curated, and formalized through expert workshops, with verification by Lean specialists.\nClarity: The paper is well organized, with clear motivation, design rationale, and transparent methodology.\nSignificance: FATE establishes the first formal benchmark exceeding PhD exam difficulty, thus setting a new standard for evaluating research-level formal reasoning.", "weaknesses": "Lack of Actionable Insight from Core Finding: The central finding is that models fail at the translation/formalization stage. However, the paper offers little new, actionable mechanism or technique to address this challenge. It merely describes the phenomenon, classifies the symptoms (hallucinations, proficiency issues), and proposes a decoupled architecture as a future direction.\n\nLimited Scope for Deeper Behavioral Analysis (General vs. Prover): The argument for the general model's superior \"effective reflection\" is compelling, but the empirical evidence for this key hypothesis relies heavily on comparing only the DeepSeek series of models. While DeepSeek-R1 significantly outperforms DeepSeek-Prover-V2 in natural language accuracy, this could be an artifact of the specific architecture/training of this lineage rather than a fundamental truth about general versus specialized models. A comparison with more diverse models, such as other specialized provers at the natural language stage (if feasible to extract for them), would significantly strengthen the claim that the general/specialized distinction is the source of the difference in \"effective reflection.\n\nWhile expert surveys are conducted, more quantitative evidence (e.g., human success rates on FATE-H/X problems) could help validate the claimed difficulty scaling.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "W8SXJqZiPp", "reviewer": "Reviewer_PLgg", "summary": "The paper lies in automated formal theorem proving with large language models (LLMs), evaluated in Lean. The authors argue that current contest-style or introductory benchmarks do not reflect research-level mathematics, and they propose a graded benchmark in abstract and commutative algebra—FATE-M/H/X—to measure progress from undergraduate to beyond PhD qualifying exam difficulty. The core question is whether we can reliably measure and drive progress toward research-level formal reasoning, and whether current systems can formalize such mathematics. The paper builds a benchmark series and a two-stage evaluation protocol to answer this. It shows very low pass rates at higher difficulty and analyzes the bottleneck between natural-language reasoning and Lean formalization.", "questions": "See Weakness", "limitations": "", "rating": 6, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "The paper tackles an important gap: modern, abstract algebra at graduate and post-graduate levels, formalized in Lean. The graded design and the curation pipeline are carefully described, with inputs from expert mathematicians and Mathlib contributors, improving both difficulty control and content quality. The two-stage analysis is informative and supports a clear technical takeaway: current systems often find a plausible informal argument but fail to turn it into correct Lean code, mainly due to library hallucinations and gaps in Lean skill. The study also includes a model comparison that proposes a reasonable training direction (decouple NL proof from autoformalization). Together, these aspects make the benchmark useful to the community.", "weaknesses": "First, the claim that FATE-X is the first formal benchmark exceeding PhD qualifying exam difficulty and surpassing Mathlib coverage is important. Although the paper provides expert survey results and internal statistics, the case would be stronger with an external audit or a direct side-by-side with other recent research-level testbeds (e.g., RealMath or FrontierMath) in terms of formalization coverage and difficulty distribution.  \n\nSecond, the baseline suite is good, but the paper’s main scientific message points to a decoupled pipeline. It would be helpful to include at least one concrete baseline that actually implements “NL proof → autoformalizer,” so that the analysis connects to an end-to-end number under the proposed design. Right now, the ablations argue for decoupling, but the paper does not show how far a simple, engineered two-module system can go on H or X.\n\nThird, library hallucinations are frequent. It would help to instrument and report “library hits” versus “misses” more explicitly: for each formal step, how often is a cited lemma present, and how often is a name or signature slightly off. A standardized “lemma grounding rate” could become a trackable metric across future systems. The current table is informative but high-level. \n\nFourth, compute and sampling fairness could be clarified. The paper uses pass@64 and long contexts; it would help to normalize sampling budgets across models of very different sizes and search strategies, and to document Lean kernel timeouts and caching settings in a machine-readable form to improve reproducibility beyond high-level text. \n\nFifth, to support the claim about coverage beyond Mathlib, a compact map of “new definitions introduced per problem” in FATE-X, with tags for the minimal Mathlib extensions that would make them solvable, would be useful for method developers. Right now we are told that new definitions are supplied in X, but a table of these would help users plan retrieval or tool-use strategies. \n\nSixth, reproducibility of the natural-language grading is described, but since this evaluation underpins the main bottleneck claim, adding a small public “adjudication set” with anonymized model outputs and gold adjudications would help outside groups reproduce the gap. The appendices outline the team and process; releasing an artifact would make the result stronger. \n\nFinally, the comparative section reports interesting behaviors of a specialized prover, including “cheating” patterns. Given the sensitivity of such claims, it would help to provide a small gallery of redacted transcripts and a measurable definition of the behaviors flagged.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "yiHjVwamBo", "reviewer": "Reviewer_uK2W", "summary": "The authors introduce FATE: a set of three benchmarks consisting of problems in abstract and commutative algebra:\n- FATE-M: 150 undergrad-level problems (published previously, here extended by 9 new problems),\n- FATE-H: 100 graduate-level problems,\n- FATE-X: PhD-qualifying problems.\n\nThe problems are presented in LaTeX and in a formal math language (Lean).\n\nA set of various LLMs are evaluated on the benchmark (including models RL-tuned for formal theorem proving in Lean).\n\nThe results are analyzed, which includes interesting qualitative study and discussion.", "questions": "1. What version of mathlib do you use for evaluation?\n2. Did you experiment with the \"decoupled\" approach you suggest where a general model is used to generate informal reasoning, and another, Lean-specific model is used to turn the reasoning into a formal proof?\n3. Did you experiment with using Lean feedback for proof repair?", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. There are not enough formal math benchmarks, especially those targeting research-level math. Therefore, benchmarks like FATE constitute valuable contribution for the research community of AI for formal math.\n2. The benchmark seems to be carefully designed and build, involving mathematicians and Lean experts -- this is important since it is relatively easy to introduce mistakes in the formal statements.\n3. The analysis of the evaluation results are informative, interesting, and quite deep.", "weaknesses": "1. The authors do not experiment with any more sophisticated inference strategies and jus use a fixed prompt and temperature to sample 64 times. It would be interesting to see, e.g., what performance can be achieved when the model receives Lean feedback for proof repair.\n2. It would be good to see more examples of problems from the benchmark to get better feeling what is included.\n3. It would be good to additionally see the performance of models from the Qwen 3 series.\n4. The authors do not specify what mathlib version they use. Different LLMs could be trained for different versions of mathlib and therefore some number of formalization mistakes may be cause by using a different version of mathlib.\n\n\n**Minor**\n* Figure 1 (a) should perhaps simply be a bar plot instead of using smoothed lines.\n* Table 2: Prover-V2 --> Goedel-Prover-V2", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)