miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward

1 Introduction

• The intended Olympiad pipeline must read an informal problem, formalize it, and produce a proof of the original statement; proving an altered problem may earn no or only partial credit.The introduction notes that formal proof-writing can take humans 10 times longer than informal proof-writing.Source: §1 · pp. 1–2
• The authors assess all 488 miniF2F problems from informal statements because compiler success does not ensure translation fidelity, and a mismatched statement can invalidate a proof.A prover failure may reflect either prover shortcomings or an incorrectly translated, harder-to-prove formal statement.Source: §1 · pp. 2–3
• 34.8% is the combined accuracy of state-of-the-art autoformalization and theorem-proving models when final proofs are checked against the original informal problems.The component accuracies reported in the literature are about 97% for autoformalization and 70.8% for Kimina Prover.Source: §1 · p. 3
• miniF2F-v2s corrects informal statements and aligns formal statements to them, while miniF2F-v2c restores original competition wording, choices, and absent solutions.For v2s, informal statements also reflect any solutions already present in formal statements; v2c retains all choices and withholds solutions when the competition problem does.Source: §1 · p. 3
• The paper releases both corrected versions and evaluates autoformalizers, theorem provers, and complete pipelines on the original and revised benchmarks.Its stated contributions include examining model shortcomings and accuracy changes across the benchmark versions.Source: §1 · p. 3

2 Reviewing the miniF2F in detail

• The section details changes to both formal and informal statements, with the distribution of changes reported in Appendix H.Source: §2 · p. 3

2.1 Errors in informal statements

• Informal statements may omit needed information or hypotheses, differ from competition originals, give wrong solutions, or omit solutions present in the formal statements.For v2s, the authors add missing solutions to the informal statements; for v2c, they remove them from the formal statements and leave a sorry for the prover.Source: §2.1 · p. 4
• The two revisions handle multiple-choice problems differently: v2s omits choices from the informal statement, while v2c places the options in the formal statement and removes the correct answer from the informal version.The v2s version therefore presents a simplified problem with a known solution, while v2c matches the original multiple-choice framing.Source: §2.1 · p. 4

2.2 Errors in formal statements

• Formal statements sometimes simplify goals or conditions, add helpful assumptions, or use incorrect types, changing the intended problem difficulty.The review distinguishes simplified and excessively simplified cases; the latter substantially alter the goal.Source: §2.2 · p. 4
• Sixteen test and validation problems were unprovable because their formal statements mistranslated the informal problems, including through missing brackets or wrong Mathlib functions.The authors identify these errors as critical to reliable theorem-prover evaluation.Source: §2.2 · p. 5

• The evaluation uses every original problem in the miniF2F benchmark to test state-of-the-art autoformalizers working with theorem provers.Source: §3 · p. 6
• For each problem, the pipeline selects the first compiler-passing formalization judged semantically faithful by human experts, then attempts a proof and checks it against the original problem.The authors call the final accuracy of the autoformalizer–prover collaboration “effective accuracy.”Source: §3 · p. 6
• Effective accuracy is considerably higher on miniF2F-v2s and v2c than v1 in the Olympiad setting, despite v2's greater difficulty.In the full-score setting, which credits excessively simplified problems, accuracy on v2 is considerably lower.Source: §3 · p. 6

• Human review rates Herald @128 at 66%, versus the 97% accuracy that the model itself marked as correct.The authors report similar evaluator differences for Kimina autoformalizer.Source: §4 · p. 6
• The evaluation covers Herald translator, Kimina autoformalizer, and o4-mini; o4-mini uses up to @10 samples but stops at the first successful compilation attempt.Herald and Kimina use @1 in the comparison described in the passage.Source: §4 · pp. 6–7
• At @128, the LLM evaluator tends to report higher accuracy than human reviewers, often treating meaning-changing statement discrepancies as negligible.The authors manually verified translations with Lean experts and report both LLM-based and human-verified accuracies.Source: §4 · p. 7
• At @1, the LLM evaluator assigns lower accuracies than human reviewers, while its estimated @128 gains are almost double the human-observed 10–15% improvement over @1.The authors hypothesize that larger sampling budgets give the LLM more opportunity to hallucinate incorrect labels.Source: §4 · p. 7
• Kimina Autoformalizer outperforms Herald Translator under both verification methods, with accuracies ranging from 78% to 88% across both miniF2F versions.Both models decline from v1 to v2, whereas o4-mini improves on the corrected dataset; the authors suggest this may indicate data contamination.Source: §4 · p. 7

• The experiments isolate whole-proof generation from autoformalization, using a sampling budget of @32 and prover-specific Lean versions.Deepseek-Prover-V1.5-RL, Goedel-Prover-SFT, and Deepseek-Prover-V2-7B use Lean v4.9.0; Kimina-Prover-Distill-7B uses Lean v4.17.0.Source: §5 · pp. 7–8
• Every evaluated prover has lower accuracy on miniF2F-v2 than v1 as reverted simplifications make theorems more challenging.The increased difficulty of v2c corresponds to an 11.2% accuracy drop for Deepseek-Prover-V2-7B.Source: Table 4 · p. 8, §5 · p. 8
• All provers solve a subset of the 16 problems repaired from their formerly unprovable form, and the authors provide formal proofs for every miniF2F-v2 problem.Source: Table 5 · p. 8, §5 · pp. 8–9
• On originally simplified problems, test accuracy drops 15–18%; on excessively simplified problems, every model loses more than 20% on test and over 30% on validation.Deepseek-Prover-V1.5-RL and Goedel-Prover-SFT lose as much as 40–50% in some cases; Kimina-Prover-Distill-7B proves 53.3% of test and 47.2% of validation problems in the excessively simplified subset.Source: Table 6 · p. 8, Table 7 · p. 9, §5 · p. 9

Autonomous AI systems excelling in reasoning and scientific discovery

• A fully automated mathematical-reasoning pipeline is proposed as a way to explore possibilities with no or minimal human intervention.The paper contrasts this with pipelines that require human formalization.Source: §6 · p. 9

Automated Theorem Proving

• Kimina Prover extended miniF2F proof lengths from roughly 10 lines for Goedel Prover to a few hundred lines using longer context.Earlier LLM theorem provers relied heavily on automated Lean solvers such as nlinarith.Source: §6 · p. 10

Autoformalization

• Autoformalization translates informal-language statements into a formal verification language such as Lean, while informalization reverses that translation.The passage describes informalization as the easier task and notes gradual improvements in LLM autoformalization accuracy.Source: §6 · p. 10

Benchmarks for formal reasoning

• miniF2F contains 488 problems sourced from textbooks and competitions including IMO, AIME, and AMC.The paper focuses on miniF2F among formal-mathematics benchmarks of varying difficulty.Source: §6 · p. 10

Reliability of mathematical benchmarks

• The paper undertakes exhaustive verification of miniF2F in response to concerns that reliable evaluation requires comprehensive, error-free benchmarks.The passage describes human-expert-verified datasets with minimal errors as “platinum benchmarks”.Source: §6 · p. 10

7 Limitations

• The study covers Lean only, despite miniF2F being available for other languages.The authors state that their informal-statement corrections apply to all miniF2F users.Source: §7 · p. 10
• The stated language limitation does not restrict the applicability of the informal-statement corrections to Lean users.The authors say those corrections apply to all users of miniF2F.Source: §7 · p. 10

8 Conclusion

• Hundreds of theorems were re-verified and changed to match their source-problem difficulty, and all sixteen unprovable original statements were fixed.The revised dataset is miniF2F-v2.Source: §8 · p. 10
• The fully automated pipeline starts from natural-language statements, and its accuracy drops significantly on miniF2F-v1.The evaluation uses state-of-the-art models from the literature.Source: §8 · p. 10
• On miniF2F-v2, the pipeline regains some accuracy lost on miniF2F-v1, which the authors attribute to the revised dataset’s higher quality.Source: §8 · p. 10
• LLM evaluation marked many autoformalizations correct despite differences from intended statements, producing a substantial gap from expert human verification.Source: §8 · p. 10
• 66% is the authors’ evaluated state-of-the-art autoformalization accuracy on miniF2F-v1, versus the reported 97%.Source: §8 · p. 10
• The authors propose miniF2F-v2 as a clearer, more demanding benchmark to guide progress in autoformalization and formal theorem proving.Source: §8 · p. 10

A Datasheet

• The dataset was taken directly from the open-source miniF2F work, and no ethical review process was conducted.Source: A Datasheet · p. 16
• The datasheet advises that the test set, and preferably the validation set, should not be used to train theorem provers or autoformalizers.Source: A Datasheet · p. 16
• The dataset is stated to be released with the camera-ready version and under the MIT license.Source: A Datasheet · p. 17
• The datasheet names supporting, hosting, or maintaining the dataset as a maintenance topic but gives no maintainer in the supplied text.Source: A Datasheet · p. 17

B Effect of a clearly structured informal proof as opposed to a vague one

• For aime_1987_p5, Kimina’s failure was reversed when given a clearer informal proof, illustrating the benefit of better proof structure for theorem provers.The example also supports the authors’ claim that miniF2F-v2 has higher-quality informal proofs.Source: B Effect of a clearly structured… · p. 18

C Wrong formalization because of unfamiliarity with the mathematical definitions in Mathlib

• For algebra_5778, Mathlib’s rpow-based nth root differs from the precollege cube-root definition, making the miniF2F-v1 formalization incorrect and unprovable; after correction, Kimina proves it.The authors provide a counterexample for a negative variable and three correct formalizations: restrict the variable to nonnegative values, define a precollege-style root, or exclude the sole possible negative root.Source: C Wrong formalization because of… · p. 19

D Examples of autoformalizer outputs on miniF2F v1 and v2

• The three modified-problem examples show that corrected informal statements can significantly affect autoformalizer performance, with outcomes depending on the kind of formalization error.The cases examine the effects of ambiguity, an unspecified proof goal, and mismatches between informal and formal statements.Source: D Examples of autoformalizer outputs… · p. 19

D.1 mathd_algebra_31

• For mathd_algebra_31, the ambiguous original statement led Herald and Kimina to fail, but an explicit recursive definition enabled Kimina—not Herald—to produce a correct autoformalization.The original omits critical details and uses an ellipsis to denote a limit ambiguously.Source: §D.1 · pp. 19–20

D.2 imo_1960_p2

• For imo_1960_p2, Herald and Kimina both correctly autoformalize miniF2F-v2s, while o4-mini’s solution-finding on v2c simplifies translation and makes proof easier, which may not earn credit.The v2c statement leaves the proof goal undefined, making translation and proving harder when modeled faithfully; v2s adds the answer to match the formal statement.Source: §D.2 · p. 20

D.3 amc12b_2003_p6

• The original informal statement is correct, but its formal version mismatches it; in miniF2F-v2s both Herald and o4-mini correctly autoformalize, while in miniF2F-v2c only o4-mini does.For miniF2F-v2c, the formal statement was changed to reflect the multiple-choice question; all options are equivalent except for their numerical solutions.Source: §D.3 · p. 20

E.1 induction_pord1p1on2powklt5on2

• The original induction problem was unprovable because of missing parentheses; miniF2F-v2 corrected the formalization by inserting them.Source: §E.1 · p. 24

E.2 aime_1990_p4

• For aime_1990_p4, the revision removes three unnecessary nonzero hypotheses absent from the informal problem, requiring provers to establish them as intermediate steps.The original formal statement included the extra hypotheses to simplify proof generation.Source: §E.2 · p. 24

E.3 amc12b_2021_p9

• All three tested provers fail on the modified logarithm theorem, whose formal statement retains each logarithm in its original base to match the AMC problem.The models are Deepseek-Prover-V1.5-RL, Goedel-Prover-SFT, and Kimina-Prover-Preview-Distill-7B.Source: §E.3 · pp. 24–25

E.4 mathd_algebra_487

• miniF2F-v2 restores the two-variable formulation over R2 for mathd_algebra_487 and removes implicit assumptions, producing a more difficult, more faithful benchmark instance.The original version used four variables and omitted the Euclidean-space context, which provided extra hints.Source: §E.4 · p. 25

F.1 imo_1983_p6

• miniF2F-v2 restores the full inequality-and-equality task for imo_1983_p6, after v1 omitted the equality condition; Deepseek-Prover-V2-7B then fails to produce a correct proof.The revised task asks models both to prove the inequality and determine the values achieving equality.Source: §F.1 · p. 27

F.2 imo_1997_p5

• For imo_1997_p5, miniF2F-v2c restores the original problem and removes the supplied goal, requiring models to find the solution and prove it; the results indicate they struggle when the goal is unknown.The passage characterizes this as solving two separate tasks.Source: §F.2 · p. 27

F.3 amc12_2000_p12

• To make problems closer to Math Olympiad settings, the authors removed correct answers from MCQ-style questions and reformulated goals to require first selecting the correct solution and then proving it.Source: §F.3 · p. 28

G Effect of introduced changes to ATP performance on Olympiad style questions

• The strongest provers solve half as many IMO problems and show a 15–50% accuracy decline on AMC in miniF2F-v2c; AIME performance drops little.Figure 3 compares four provers across three versions and shows the total problems in each dataset.Source: Figure 3 · p. 29, G Effect of introduced changes to ATP… · p. 29

H Statistics about our modifications

• Approximately 40% of formal statements contained an error, while most problems in both sets were simplified and did not reflect their intended difficulty.Figure 4 presents the distribution of identified formal and informal statement errors across the test and validation sets.Source: Figure 4 · p. 30, H Statistics about our modifications · p. 30

I Failure topics of tested autoformalization models

• Lean experts manually classified autoformalization failures, except translations not validated by Lean4 REPL, which failed compiler verification.Tables 9–11 report error frequencies for HERALD, Kimina-autoformalizer, and o4-mini on miniF2F-test.Source: I Failure topics of tested… · p. 31, Table 9 · p. 31, Table 10 · p. 31

J Toward improving autoformalization models

• Rigorous evaluation on high-quality, discrepancy-free benchmarks is presented as a crucial first step toward improving autoformalization models.Source: J Toward improving autoformalization… · p. 32
• Training data should align formal and informal statements; discrepancies can introduce noise, and miniF2F validation is frequently reused for training.The passage says misaligned examples may negatively influence model accuracy and generalization.Source: J Toward improving autoformalization… · p. 32
• Training-corpus distribution, architecture, reasoning mechanisms, context length, and automated feedback may affect performance, motivating systematic ablations.The authors identify data quality, architecture, and reasoning modules as components for ablation studies; reliable benchmarks are needed to interpret them.Source: J Toward improving autoformalization… · p. 32

K Responsibility statement and License information

• The authors plan to release the dataset under the MIT license on GitHub and Hugging Face.Source: K Responsibility statement and License… · p. 32