PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Jiedong Jiang, Wanyi He, Yuefeng Wang, Guoxiong Gao, Yongle Hu, Jingting Wang, Nailin Guan, Peihao Wu, Chunbo Dai, Liang Xiao, Bin Dong

arXiv:2511.02872v4cs.LGcs.AIcs.FLcs.LO

TL;DR

Existing benchmarks focus largely on contest or introductory mathematics, leaving advanced research-level formal reasoning underrepresented. FATE introduces a progressive formal algebra benchmark series and evaluates models’ natural-language reasoning alongside formalization. Models’ formalization accuracy is very low on FATE-H and FATE-X, and natural-language reasoning is more accurate than formal proof generation.

  • Problem

    Existing benchmarks largely target contest-style or introductory mathematics rather than the abstraction and theoretical frameworks characteristic of advanced research.

    Source: §1 · pp. 1–2

  • Method

    The paper introduces progressively difficult formal algebra benchmarks and evaluates model outputs through natural-language reasoning assessment and automated Lean verification.

    Source: §1 · pp. 2–3

  • Results

    Formalization reaches only 3% (Pass@64) on FATE-H and 0% on FATE-X, while natural-language reasoning is more accurate than formalization.

    Source: §1 · p. 3, §5 · p. 10

  • Takeaways & Limitations

    FATE provides a graded benchmark series intended to establish checkpoints toward research-level formal mathematical reasoning.

    Source: §1 · pp. 2–3

    Rigorously confirming the proposed research directions remains beyond the scope of this article.

    Source: §4.6 · p. 10

Abstract

from arXiv · show

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

1 Introduction

Existing formal theorem-proving benchmarks largely cover contest mathematics or introductory university material, leaving a gap in assessing advanced mathematical research. FATE introduces progressively harder formal algebra benchmarks and evaluates both natural-language reasoning and formalization, finding low formalization accuracy and a gap between the two stages.

1 Introduction

  • The benchmark series addresses a gap left by contest-style and introductory mathematics benchmarks, which differ from modern research in abstraction and use of theoretical frameworks.Advanced mathematics involves broad, deeply nested abstract concepts and exploration of new insights and theoretical frameworks.Source: §1 · p. 2
  • DeepSeek-Prover-V2 exhibits less effective natural-language reflection than general-purpose models, reducing its accuracy at that stage.The comparison is between the specialized prover and general-purpose models including DeepSeek-R1.Source: §1 · p. 3
  • FATE-H and FATE-X extend formal algebra evaluation from undergraduate material to beyond PhD qualifying-exam difficulty, with FATE-X also exceeding Mathlib’s formalization coverage.Each new benchmark contains 100 problems.Source: §1 · pp. 2–3
  • Top models achieve only 3% (pass@64) on FATE-H and 0% (pass@64) on FATE-X, while natural-language reasoning is significantly more accurate than formalization.The evaluation mirrors a two-stage process, assessing natural-language Chain-of-Thought with expert review and final Lean code with automated verification.Source: §1 · pp. 2–3
  • Mathlib hallucinations and Lean proficiency issues are the most common formalization errors, while general capability issues occur at intermediate frequency and misalignment is least common.The paper classifies these errors through a two-stage analysis of model outputs.Source: §1 · p. 3

2 Related Works

Prior mathematics benchmarks range from elementary problems to research-level work, while formal benchmarks cover contests, university mathematics, and specialized domains. A common limitation is reliance on final-answer verification.

2 Related Works

3 The FATE Benchmark Series: Design and Curation

FATE is a graded formal algebra benchmark series spanning undergraduate exercises through PhD qualifying-exam-level and beyond. Its curation combines expert mathematical selection, Lean formalization, and review; benchmark characteristics support a difficulty progression and include problems requiring definitions beyond Mathlib.

3 The FATE Benchmark Series: Design and Curation

  • FATE comprises FATE-M, FATE-H, and FATE-X, with 150 problems in the expanded FATE-M and 100 each in the two newly introduced benchmarks.The series progresses from textbook exercises through honors or graduate-level problems to PhD qualifying-exam level or beyond.Source: §3 · p. 4
  • FATE focuses on abstract and commutative algebra, emphasizing abstract proofs and algebraic structures rather than equation-solving or numerical computation.The paper describes this domain as self-contained and suitable for deep problem-solving without extensive input from other fields.Source: §3 · p. 4

3.1 Benchmark Curation

  • FATE-H and FATE-X problems draw on textbooks, university qualifying and honors exams, research papers, and advanced community resources such as the Stacks Project.Source: §3.1 · p. 4
  • The H/X curation workflow collected and classified 400 candidates, formalized 200 selected problems in Lean, then reviewed and corrected the formalizations.The process involved nearly twenty algebra postdocs and PhDs, five experienced Lean specialists, and two reviewers; external Lean community experts also assisted verification.Source: Figure 2 · p. 4, §3.1 · p. 5

3.2 Benchmark Characteristics

  • FATE-X shifts topic coverage toward advanced commutative algebra, while FATE-H emphasizes abstract algebra.Source: §3.2 · p. 5
  • Case studies describe a progression from direct theorem application in FATE-M to integrative reasoning in FATE-H and recursive structural analysis in FATE-X.The examples involve similar mathematical topics at increasing difficulty.Source: §3.2 · p. 5
  • Human participants achieved 73% accuracy on FATE-H and 21% on FATE-X; algebra professors also rated FATE above classical textbooks and ProofNet in difficulty, coverage, and originality.Participants were algebra PhD students or postdocs given five non-overlapping natural-language problems to solve in 2.5 hours; 7/10 professors judged FATE suitable for or harder than standard algebra qualifying exams.Source: §3.2 · p. 5
  • 38% of FATE-X problems require new definitions absent from Mathlib, averaging 2.4 definitions in that subset, and successful solutions may require deriving lemmas or formulating definitions.The benchmark files are self-contained, depend only on Mathlib, and follow strict Lean formalization standards.Source: §3.2 · pp. 5–6

4 Experiments and Results

Experiments find very low formal success on FATE-H and FATE-X, with natural-language reasoning substantially more accurate than formalization. Analyses identify translation into formal language as a key bottleneck and compare general-purpose models with specialized provers.

4.2 Benchmark Performance

  • 3 of 100 FATE-H problems were solved by the best model, while no model produced valid Lean proofs on FATE-X.The evaluation used pass@64; Table 1 covers formalization accuracy across FATE benchmarks.Source: §4.2 · p. 6, Table 1 · p. 6

4.1 Experiment Setup; 4.2 Benchmark Performance

  • Models commonly generated a natural-language proof before formalization, and the evaluation used whole-proof generation with pass@64 and a 64k-token limit.Formal proofs were checked by the Lean kernel, with additional checks for theorem transcription and generated lemmas.Source: §4.1 · p. 6, §4.2 · p. 7

4.3.1 Manual Evaluation of Natural Language Proofs

  • Manual evaluation found a significant gap between natural-language proof correctness and final formalization, while the analysis compared pass@1 reasoning with pass@64 formal accuracy.The manual evaluation assessed models’ natural-language proofs under the original task settings.Source: §4.3 · p. 7, §4.3.1 · p. 7, Table 2 · p. 7

4.3.2 Ablation Study on the Impact of Prompts

  • Natural-language mathematical ability was higher without a formal-proof prompt, but requiring “math-before-lean” had almost no impact on DeepSeek-R1 accuracy.The prompt ablation was designed to test whether formalization instructions suppress natural-language mathematical ability.Source: §4.3.2 · p. 7

4.3.3 Analysis of Main Findings

  • Across tested models, intermediate natural-language reasoning accuracy far exceeded formalization accuracy, pointing to translation and implementation—not mathematical ability—as the primary bottleneck.The analysis also found formalization attempts highly aligned with their preceding natural-language reasoning.Source: §4.3.3 · p. 8

4.4 Formalization Error Analysis

  • Among mathematically correct but formally incorrect attempts, Mathlib hallucinations and Lean proficiency issues were most common, while misalignment was infrequent.The error counts used whole proofs whose intermediate natural-language proofs were judged correct; DeepSeek-Prover-V2 data were excluded for header-related issues.Source: §4.4 · p. 8

4.5 General Models vs. Theorem Provers

  • General-purpose reasoning models outperformed specialized provers in natural-language success, while DeepSeek-Prover-V2 lacked effective reflection and exhibited non-aligned behaviors.DeepSeek-R1 sometimes located, diagnosed, and repaired flaws; DeepSeek-Prover-V2’s reflections could change approach without changing the underlying logic.Source: §4.5 · p. 9

4.6 Implications and Discussion

  • The authors propose separating natural-language reasoning from autoformalization and identify balancing formal accuracy with effective, aligned reasoning as a future challenge.Rigorously confirming these proposed research directions remains beyond the article’s scope.Source: §4.6 · pp. 9–10

5 Conclusions

The conclusions present FATE as a graded algebra benchmark series for advanced mathematical reasoning and report severe formal-reasoning limits alongside a formalization bottleneck. Supporting material describes Lean formalization and examines benchmark quality, problem types, topic distribution, and progressive difficulty.

5 Conclusions

  • FATE-H and FATE-X extend a graded formal algebra benchmark series focused on frontier research, where evaluated models achieved maximum pass rates of 3% on FATE-H and 0% on FATE-X.The conclusion attributes the main bottleneck to formalization and identifies library hallucinations and insufficient Lean proficiency as common errors.Source: §5 · p. 10

A Introduction to Formalization and Lean

  • Mathematical formalization translates informal ideas into precise logical language; in Lean, tactics manipulate proof states and generate low-level proof code once goals are solved.Mathlib’s broad algebra coverage makes Lean suitable for formalizing advanced mathematics.Source: A Introduction to Formalization and Lean · p. 15

B Benchmark Quality Analysis

  • The benchmark-quality analysis uses illustrative examples, diversity and difficulty statistics, and an expert survey to assess mathematical content.It also includes examples from FATE-M and, for content-focused analyses, presents natural-language problem statements without formalization details.Source: B Benchmark Quality Analysis · p. 16

B.1 Representative Examples

  • Representative examples include proving polynomial rings preserve complete integral closure, coprime-power equality in domains, and a finite-field rational-function extension is Galois..Source: §B.1 · pp. 16–17

B.2 Diversity

  • The appendix organizes benchmark diversity around problem types and mathematical-domain distributions.These are presented as principal dimensions of the series’ diversity analysis.Source: §B.2 · p. 17

B.2.1 Problem Types

  • Abstract reasoning problems are most common in FATE-H and FATE-X, but a problem’s abstractness does not directly correlate with its mathematical difficulty.The listed types also include concrete-example problems and open constructive problems.Source: §B.2.1 · p. 17

B.2.2 Domain Statistics

  • The topic distribution shifts from abstract algebra in FATE-H toward advanced commutative algebra topics in FATE-X.Table 4 is identified as the distribution of problems by mathematical topic in FATE-H and FATE-X.Source: §B.2.2 · p. 17, Table 4 · p. 18

B.3 Progressive Difficulty

  • The progressive-difficulty analysis uses examples of increasing difficulty and statistics on model output-token length and natural-language accuracy.Those statistics are presented as indicators of problem difficulty.Source: §B.3 · p. 18

B.3.1 Case Study: A Graded Challenge on Non-Simple Groups

A case study traces how DeepSeek-R1’s proof structure grows from direct deduction on FATE-M to integrative reasoning on FATE-H and recursive analysis on FATE-X. The progression reflects deliberately increasing proof complexity.

B.3.1 Case Study: A Graded Challenge on Non-Simple Groups

  • On FATE-X, the model must examine the relationship between Sylow 17-subgroup normalizers and Sylow 3-subgroups after earlier analyses leave possibilities unresolved.This further analysis follows examination of all prime factors and a counting argument.Source: §B.3.1 · p. 18
  • On FATE-H, a single-prime Sylow approach is insufficient; the model combines results for all prime factors with a counting contradiction.The resulting proof has a tree-like dependency structure whose exploratory branches converge in a synthetic conclusion.Source: §B.3.1 · pp. 18, 20
  • On FATE-M, the model applies Sylow’s theorem to one prime and reaches the conclusion directly from the given conditions.The proof is represented as a simple sequential dependency chain.Source: §B.3.1 · pp. 18, 20
  • Figure 4 maps the progression across FATE-M, FATE-H, and FATE-X, with blue, orange, and green marking theorem application, synthesis, and exploration.The X-level proof adds nested re-analysis after initial analysis proves insufficient.Source: Figure 4 · p. 20, §B.3.1 · p. 20
  • FATE-M, FATE-H, and FATE-X require a progression from linear deduction to integrative reasoning to recursive structural analysis.The case study attributes the difficulty gradient to deliberately designed proof structures.Source: §B.3.1 · p. 20

B.3.2 Auxiliary Statistics on Proof Difficulty

Auxiliary statistics show that DeepSeek-R1’s intermediate natural-language accuracy declines from FATE-M to FATE-H to FATE-X, while output token lengths rise across those levels. The intermediate accuracy trend does not directly measure standalone natural-language performance.

B.3.2 Auxiliary Statistics on Proof Difficulty

  • DeepSeek-R1’s intermediate natural-language Pass@1 accuracy decreases from FATE-M to FATE-H to FATE-X.These are expert evaluations of the natural-language solutions produced before formalization; Table 5 reports the accuracy.Source: §B.3.2 · p. 21, Table 5 · p. 21
  • The decreasing intermediate-accuracy trend persists even though a pure natural-language task yields higher accuracy than the intermediate output.The reported improvement is significantly smaller than the gap between benchmark levels, so it does not change the observed trend.Source: §B.3.2 · p. 21
  • Average output token length rises from FATE-M to FATE-H to FATE-X across all models.Table 6 presents average output token length on the three benchmarks.Source: §B.3.2 · p. 21, Table 6 · p. 21

B.4 Expert Assessment

In expert comparisons, FATE was favored over textbook and ProofNet problem sets on difficulty, coverage, originality, and research-evaluation dimensions, while ratings of its PhD-exam suitability were more mixed. The appendix also describes cases where formalization prompts revision of natural-language reasoning, but concludes that the stages remain functionally separate.

B.4 Expert Assessment

  • FATE was selected by 10/10 experts as the most difficult set, 8/10 for best coverage, and 9/10 for testing deep understanding, originality, and research-evaluation ability.The comparison used topic-balanced samples from FATE-H/X, classical algebra textbooks, and ProofNet.Source: §B.4 · p. 21
  • For PhD qualifying exams, 7/10 experts rated the sampled problems as meeting or exceeding the level, while 4/10 judged the coverage complete.Another 3/10 said coverage was mostly complete with no important points omitted; most experts recognized the set as meeting or exceeding PhD-exam difficulty.Source: §B.4 · p. 22

C.1 Interaction Between Natural Language Reasoning and Formalization

Output of DeepSeek-R1 (FATE-X)

  • A model may also abandon a valid natural-language proof when it is poorly suited to formalization and devise an alternative strategy.The paper interprets these feedback cases as supporting functional separation: formalization sends the task back for logical revision rather than repairing the logic itself.Source: Output of DeepSeek-R1 (FATE-X) · p. 23
  • The authors describe a decoupled two-stage research approach as promising, with natural-language proof generation separate from autoformalization.Their reasoning is that intermediate natural-language accuracy differs across models and from pure natural-language accuracy, while formalizations align with preceding reasoning.Source: Output of DeepSeek-R1 (FATE-X) · p. 23

C.2 Ablation Study of Prompts

Prompt ablations on FATE-X find that including Lean generation reduces natural-language reasoning accuracy, while formal context has a smaller effect and an explicit math-first instruction has almost none. The appendix also characterizes common natural-language error types and reports variation in models’ explored proof strategies.

C.2 Ablation Study of Prompts

  • Including Lean generation significantly decreases DeepSeek-R1’s natural-language reasoning correctness, while showing the formal statement has a smaller negative effect.The comparison uses Prompts 1 and 3 for the formalization task and Prompts 2 and 3 for formal context.Source: §C.2 · p. 23
  • Requiring a math-first output has almost no effect: Prompt 4 results were nearly identical to the baseline Prompt 1.Table 7 reports natural-language accuracy under the different prompts.Source: §C.2 · p. 23, Table 7 · p. 23

C.3.1 Gap

  • A Gap error leaves a key non-trivial step unproved, often by assuming a needed lemma or invoking an overly powerful theorem.In the example, the model’s counting argument depends on proving distinct Sylow subgroups have trivial intersection, which it skips.Source: §C.3.1 · p. 24, Model Output (DeepSeek-Prover-V2) · p. 24

C.3.2 Hallucination

  • A Hallucination is an explicit false mathematical statement; on the Gorenstein example, all tested models made the same socle-condition error.The authors suggest this repeated mistake reflects a shared knowledge gap in specialized algebraic theory.Source: §C.3.2 · p. 24, Model Output (DeepSeek-R1) · p. 24

C.3.3 No Progression

  • No Progression means no substantive mathematical advance; in one FATE-X case, the model restated a theorem equivalent to the problem.Almost all pass@16 attempts on that problem made no progress, which the authors say may help differentiate model capabilities.Source: §C.3.3 · p. 24, Model Output (DeepSeek-R1) · p. 25

C.3.4 Reasoning Problem

  • A Reasoning Problem uses largely correct mathematical facts but connects them through flawed logic.The authors distinguish these errors from failures primarily involving mathematical knowledge or strategy.Source: §C.3.4 · p. 25

C.4 Variance in Natural Language Reasoning

  • On an open-ended FATE-X problem, the model initiated three distinct viable proof routes, although it erred in later steps of two non-standard routes.Expert mathematicians confirmed all three approaches were viable strategies.Source: §C.4 · p. 25, Problem Statement · p. 25

Problem Statement

  • The three approaches ranged from a standard Kummer-theory construction to a more abstract argument and a cyclotomic-extension shortcut.The standard approach appeared most frequently, and the authors report that diverse strategy discovery can be tested despite imperfect execution.Source: Problem Statement · pp. 25–26

D Analysis of Formal Language Output

The appendix characterizes formalization errors through category descriptions and examples, then examines model behavior on FATE-X problems involving novel definitions.

D Analysis of Formal Language Output

D.1 Detailed Formal Errors

  • Mathlib hallucinations include inventing unavailable theorems or instances, guessing lemma names incorrectly, and misjudging a function’s conclusion form.These errors can involve a theorem, definition, or typeclass instance that does not exist or is used incorrectly in context.Source: §D.1 · p. 26
  • Lean proficiency issues include misunderstandings of Lean design and formal disciplines, syntax or type problems, and mispredictions of tactic outcomes.Complex simp outcomes may be difficult to predict without interactive execution.Source: §D.1 · p. 26
  • General capability issues include violating instructions, repeating proof patterns, leaving sorry placeholders, and syntax errors that prevent compilation.The examples include altered statements or imports, loops that do not advance a proof, and incomplete formal arguments.Source: §D.1 · p. 26
  • Misalignment occurs when a formal proof departs from prior mathematical reasoning; one example abandons a correct approach to proving sin(π/180) algebraic.The model instead followed a mathematically incorrect path.Source: §D.1 · pp. 27–28
  • The appendix’s partial proof example illustrates formal errors including incorrect Mathlib naming, Lean design or type issues, repetitive tactics, and unfinished sorry steps.The examples include an incorrect naming convention, syntactic or type-related problems, repeated proof attempts, and remaining sorry placeholders.Source: §D.1 · p. 27

D.2 Case study on FATE-X

  • FATE-X case-study errors were consistent with FATE-H, while models seldom introduced reusable lemmas about novel mathematical properties in problem definitions.The analysis focused on DeepSeek-R1 because of DeepSeek-Prover-V2’s structured-output tendency.Source: §D.2 · p. 28
  • DeepSeek-R1’s new definition merely abbreviated an object already in the problem, and its later basic-property lemmas did not establish the novel properties.The example illustrates the broader absence of lemmas about the new mathematical properties in the problem statement.Source: §D.2 · p. 28

E Comparative Analysis: General Models vs. Theorem Provers

The comparison finds DeepSeek-R1 more accurate in natural-language reasoning than DeepSeek-V3 and DeepSeek-Prover-V2, and examines how the models reason and formalize proofs. It also describes the generation and verification setup.

E Comparative Analysis: General Models vs. Theorem Provers

E.1 Analysis of Behaviors during the Reasoning Process

  • All three DeepSeek models often begin reasoning with similar approaches and sometimes fall into the same traps; in one case, Prover-V2 later adopts an independent strategy.The models initially consider Galois action in the cyclotomic field, although the most direct solution does not require that background.Source: §E.1 · p. 29, Model Output (DeepSeek-V3) · p. 30

Model Output (DeepSeek-V3)

  • DeepSeek-V3 may skip details or fabricate intermediate conclusions rather than deeply analyze a problem’s core challenge.The paper frames reflection as locating, diagnosing, evaluating, and repairing flaws in an argument; in one example V3 cites irreducibility as a known result instead of proving it.Source: Model Output (DeepSeek-V3) · pp. 30–31

Model Output (DeepSeek-Prover-V2)

  • DeepSeek-Prover-V2 can switch approaches without effectively evaluating or correcting them, hindering long-chain arguments.In an example, it moves among counting and group-action arguments, then returns to its initial approach; the analysis describes this reflection as formalistic rather than substantive.Source: Model Output (DeepSeek-V3) · p. 31, Model Output (DeepSeek-Prover-V2) · p. 31

Model Output (DeepSeek-R1)

Model Output (DeepSeek-R1*)

  • In a trial-and-error example, DeepSeek-R1 moves toward constructing an ideal over the reals and connecting the problem to Hilbert’s Nullstellensatz.Its initial constructions using points over the complex field were invalid or led to the trivial ideal.Source: Model Output (DeepSeek-R1*) · p. 32

E.2 Misaligned Behaviors in Natural Language Reasoning Process

  • Examples of misaligned behavior include bypassing a proof with sorry and treating a conflict over Lean’s definition of Ideal.height as evidence that the problem statement is flawed.The latter example reflects a misunderstanding of the formal library’s definition.Source: Model Output (DeepSeek-Prover-V2) · p. 33

F.1.2 Verification

  • Generation used API-served models with a 64k-token maximum; verification required passing string checks and Lean-kernel checks, with no sorry or compilation errors.Mathlib versions varied by benchmark, and the Lean timeout was 300 seconds.Source: §F.1.1 · pp. 33–34, §F.1.2 · p. 34

F.1.3 Additional Pass@k Results

The appendix reports additional Pass@k and normalized-budget evaluation procedures, describes expert review of natural-language proofs, and lists prompts used for different model outputs.

F.1.3 Additional Pass@k Results

  • Pass@k results are reported for FATE-M and FATE-H, while FATE-X is omitted because no model produced a successful proof.The estimates use 64 samples per problem and an unbiased estimator introduced in Chen et al. (2021).Source: §F.1.3 · p. 34

F.1.4 Performance under Normalized Budget

  • The normalized-budget comparison estimates cost as model size multiplied by average output tokens and number of samples, excluding closed-source models and FATE-X.FATE-X is omitted because all recorded values were zero; Table 10 is identified as the normalized-budget accuracy comparison.Source: §F.1.4 · p. 34, Table 10 · p. 36

F.2.1 Evaluator Qualifications

  • Natural-language proof evaluators were algebra PhDs or postdoctoral researchers with experience grading university-level mathematics exams.The workflow aimed to assess proof validity objectively and consistently.Source: §F.2.1 · p. 35, §F.2.2 · p. 35

F.2.2 Evaluation Workflow and Standards

  • Evaluators first studied the ground-truth proof, then judged the model’s natural-language proof while disregarding formalization code and its errors.The paper notes that proof validity judgments rely on evaluators’ professional knowledge and subjective judgment.Source: §F.2.2 · pp. 35–36
  • For long outputs, evaluators located the model’s final proof and reconstructed its supporting argument from relevant reasoning elsewhere in the output.They based the final judgment on the reconstructed complete chain of reasoning.Source: §F.2.2 · p. 36

F.3 Judgment and Attribution

  • Evaluators recorded proof validity, core errors for failed proofs, and optional remarks about model performance.The remarks supplied qualitative observations about models’ thought patterns.Source: §F.3 · pp. 36–37

Baseline Prompt

  • The baseline and Math-before-Lean prompts request Lean code, with the latter also requiring a natural-language proof; the Prover-V2/Goedel prompt requests a proof plan before code.The baseline instructs models not to change the original statement, while the Prover-V2/Goedel prompt asks for key steps and intermediate lemmas.Source: §G.1 · p. 37, Baseline Prompt · p. 37, DeepSeek-Prover-V2(CoT)/Goedel Prompt · p. 37

Pure Math Prompt

  • The Pure Math prompt requests a complete, detailed natural-language proof, while the Math Output and Kimina prompts request step-by-step reasoning for a Lean-stated problem.The Math Output prompt asks for a final answer after careful reasoning; Kimina’s prompt includes a formal statement after its natural-language problem.Source: Pure Math Prompt · p. 37, Kimina Prompt · p. 37, Math Output Prompt · p. 38
Loading 2511.02872v4…