miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward
Authors: Azim Ospanov
Farzan Farnia
Roozbeh Yousefzadeh
Venue: NeurIPS 2025 poster ()
Keywords: formal reasoning
automated theorem proving
lean prover
ai for math
Primary area: machine_learning_for_sciences

Abstract: We perform a thorough analysis of the formal and informal statements in the miniF2F benchmark from the perspective of an AI system that is tasked to participate in a math Olympiad consisting of the problems in miniF2F. In such setting, the model has to read and comprehend the problems in natural language, formalize them in Lean language, then proceed with proving the problems, and it will get credit for each problem if the formal proof corresponds to the original informal statement presented to the model. Our evaluation results reveal that the best accuracy of such pipeline can be about 36% using the SoTA models in the literature, considerably lower than the individual SoTA accuracies, 97% and 69% reported in the autoformalization and theorem proving literature. Analyzing the failure modes, we trace back a considerable portion of this drop to discrepancies between the formal and informal statements for more than half of the problems in miniF2F. We proceed with correcting all the errors, discrepancies and simplifications in formal and informal statements, and present the _miniF2F-v2_ with fully verified formal and informal statements and proofs. Evaluating the full theorem proving pipeline on _miniF2F-v2_ leads to the best accuracy of 70%, a significant improvement from the 40% on the original miniF2F, yet indicating considerable misalignment between the autoformalization models and theorem provers. Our deep analysis suggests that a higher quality benchmark can help the community better evaluate progress in the field of formal reasoning and also better diagnose the failure and success modes of autoformalization and theorem proving models. Our dataset is available at https://github.com/roozbeh-yz/miniF2F_v2.

miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward
Azim Ospanov aospanov9@cse. cuhk edu hk
Farzan Farnia cuhc
Roozbeh Yousefzadeh roozbeh, y28gmail com
farnia@cse. cuhk. edu hk
Abstract
We perform a thorough analysis of the formal and informal statements in the miniF2F benchmark from the perspective of an Al system that is tasked to partici- pate in math Olympiad consisting of the problems in miniF2F. such setting, the model has read and comprehend the problems in natural language, formalize them in Lean language, then proceed with proving the problems, and it will get credit for each problem if the formal proof corresponds the original informal statement presented to the model. Our evaluation results reveal that the best accu- racy of such pipeline can be about 36% using the SoTA models the literature, considerably lower than the individual SoTA accuracies, 97% and 69% reported in the autoformalization and theorem proving literature. Analyzing the failure modes, we trace back a considerable portion of this drop to discrepancies between the formal and informal statements for more than half of the problems in miniF2F. We proceed with correcting all the errors, discrepancies and simplifications in formal and informal statements, and present the miniF2FFv2 with fully verified formal and informal statements and proofs. Evaluating the full theorem proving pipeline on miniF2F-v2 leads the best accuracy of 70%, a significant improvement from the 40% on the original miniF2F, yet indicating considerable misalignment between the autoformalization models and theorem provers. Our deep analysis suggests that higher quality benchmark can help the community better evaluate progress in the field formal reasoning and also better diagnose the failure and success modes of autoformalization and theorem proving models. Our dataset is available at battps://git com/roozbeh baaeeeh-yy//aa yz/ htt//mnniFF..... _2
1 Introduction
Automated reasoning with computers has long and rich history [1] and with the rise of AI, has had major advancements in the past decades, notably DeepBlue (2). AlphaGo [3], etc. Shortly after the rise of Large Language Models (L.LMs), 4 showed the remarkable ability of these models to learn the language of formal verification systems such as Lean 5 and automatically prove mathematical theorems formal language, building on prior work such as 6 This gave rise the subfield of Automated Theorem Proving (ATP) in the machine learning literature which has seen considerable advancements in the past few years 77. The shared progress in this field was partly made possible by the miniF2F benchmark [ which consists of 488 theorems in formal and informal languages drawn from prestigious mathematical competitions and Olympiads.
Writing mathematical proofs in formal language makes the verification of proofs automated and reliable, however, learning and writing the language of formal verification systems is not easy for humans nor for the LLMss. For a human, it might take 10 times longer to write proof in formal language compared to an informal one. LLMs, on the other hand, are likely to excel at learning these
Huawei Hong Kong Research Center Department Computer Science & Engineering, The Chinese University of Hong Kong
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

Math Olymgjadk
Cose CuedtiTomee Fomral sifrerst nel pass the loin verifittinn
AAA
XA
jodg
AIME
AI
MO
Case 42 Evcraal statonert paice
varii sion but totthheggee prover Fails
MATHENATICN OLY
Judge
Anrueee with Fernal suth systems
Caso Formal sianeeerr ditiowal lan the iiternal essereent
Problem
A
Carrect
proversscceeds
A00
joder
estpel
Figure 1: High-level overview of formal math prover system operating in a Math Olympiad setting.
formal languages, and combined with other automated reasoning tools, they may help automate the process of mathematical reasoning. This has given rise to of the main goals of the community: developing AI systems that can compete with humans in major mathematical Olympiads [9]. For example, in 2024, AlphaProof was able to reach the level of silver medal at the International Math Olympiad (IMO) [0]. Reaching that level of automated reasoning requires a model to automatically read mathematical problem in informal language, formalize it in a formal verification language, and generate a correct formal proof that can pass the verification system.
Such automated system would fail if it changes the original problem statement and proves altered version of the competition problem, the same way that a human participant proves simplified version of problem will likely get no, or at the most, a partial credit not sufficient for medal. Therefore, having models that can correctly translate to formal language is crucial, otherwise, there will be need for human in the loop perform the formalizations. This translation, known as autoformalization in the literature, has seen major advancements on the miniF2F benchmark (TT.
While the miniF2F benchmark has enabled advancements both in ATP and in autoformalization, over the years, has also been reported have certain limitations, such as wrong formalizations, unprovable theorems, etc. Most recently. [12) reported fixing errors in 5 theorems of miniF2F which had made them unprovable. The community on autoformalization has also reported certain inconsistencies between the formal and informal statements in mf 13 This motivates to conduct deep analysis of this benchmark from the holistic perspective described above. In this framework, an AI system is tasked with participating in a miniF2F competition. The system must prove all 488 theorems in the benchmark from their informal statements, with the goal of producing correct proof's for the original formulations. Figure T illustrates the stages at which failures can prevent an Al system from arriving at a correct solution in a Math Olympiad setting:
Autoformalization failure: The autoformalizer fails to write formal statement that passes the formal verification compiler, e.g., Lean. In this case, the output of the autoformalizer cannot be passed to the prover, and the Al pipeline fails automatically.
Translation failure: The autoformalizer produces formal statement that passes the compiler error-free. However, the formal statement does not match the informal one, i.e., the translation not accurate. Such formal statement will then be passed the prover model. If the prover model fails to prove the problem, the pipeline automatically fails. However, if the prover model succeeds in proving such a formal statement, the judge will not give credit to the proof because it does not correspond to the original problem in the Olympiad. This is the case most prone to being neglected and inaccurately counted toward the success of Al models without a human expert examining the final proof.

---

3. Prover failure: The prover fails to prove, leading to the automatic failure of the Al pipeline. If the autoformalized statement is a correct translation of the informal one, this failure can be interpreted as a shortcoming of the prover model. However, it may be the case that the formal statement is incorrectly translated by the autoformalizer, making it unprovable or more difficult than the original problem, and such mistranslation may be the root cause of the prover's s failure. In the latter case, the failure of the end-to-end pipeline may be attributed to the autoformalizer.
In this work, we build such an automated pipeline by using the SoTA models for autoformalization and for theorem proving. While the accuracy of the best autoformalization model on miniF2F is reported be about 97% [4), and the accuracy of Kimina Prover on miniF2F is 70.8% [12]. the combined accuracy of these models leads to an accuracy of 34.8% after comparing the final proofs with the original problem statements in informal language. This significant drop in accuracy comes from several sources which we will examine in detail, two of which account for most of the failures. Our extensive human evaluation of autoformalization results, across five models, reveals that their autoformalization accuracy is not as high as the ones reported in the literature, because those reported accuracies often evaluated by L.MS and not by human familiar with the formal language. The other reason for this major drop is that the formal statements in miniF2F. i.c., the starting point of the automated system, are often significantly simplified compared the informal statements, and hence, when more faithful translations are given to ATPs, the theorems turn out to be more difficult, making the ATPs more likely to fail. Therefore, we observe a disconnect between the ATP literature and the autoformalization literature.
We analyze every failure mode of an end-to-end formal reasoning pipeline on the miniF2F benchmark and correct over 300 Lean 4 statements to eliminate errors and simplifications. Since our starting point is the original miniF2F. and miniF2F-v2c. For miniF2F-v2s, where 8 stands for simplified, we only correct the mistakes in the informal statements and then modify the formal statements to exactly match the informal ones. This version is closer to miniF2F-v1, yet all theorems are correct and provable, and there are no discrepancies between the informal and formal statements. For all the problems where the formal statement contains the solution, we make sure the informal statements reflect the solutions as well.
take steps to modify it, leading to variations: miniF2F-v2s
We then take another step which leads miniF2F-v22 where stands for competition. Here, change the informal statements to reflect the exact statements in the original competitions for all the problems from IMO and AMC. If a problem has multiple choices, we keep all the choices in the informal statement and also include the choices in the formal one. Hence, the model has to first choose the correct choice and then prove it, adding an extra level of difficulty to the theorems. When original informal statement does not provide a solution and asks for the participant to first find the solution and then prove it, we also do not provide the solution in the informal and formal statements.
Our contributions are as follows:
We release two corrected versions of m2 benchmark (both test and validation sets): simplified and competition-level. All the informal and formal statements are manually checked to exactly correspond each other.
We perform thorough evaluation of autoformalization models miniF2F-v1, v2s, and v2c, demonstrating the current shortcomings in the evaluation practices in the autoformalization literature well as the benefits of miniF2F-v2s and v2c.
We perform a thorough evaluation of miniF2F-v2s and v2c for the task of ATP reporting that the accuracy of SoTA models drop significantly on the problems that were excessively simplified, yet their accuracy increases on the subset of problems that were previously unprovable because of formalization errors.
We further evaluate a complete automated pipeline of SoTA models on the task of theorem proving starting from informal statements and report their accuracy both on the original version of miniF2F and miniF2F-v2 demonstrating the better accuracy of such pipelines on miniF2F-v2.
2 Reviewing the miniF2F in detail
In this section, we detail various types of changes that we made in the original miniF2F benchmark for both formal and informal statements. Detailed information about the distribution of made changes can be found in Appendix H
3

---

Correction of ammel2b_20 2__2_p22333
mimiF2F-11
miniF2FF-22
miniF2F-v2e
Suppose
Suppose
Suppose
2
21
What is the value of xt? Show that
following options.
3
14
37
(A)
(C)
15
3 (A)
14
37
52
Show that
/-Formal statement-/
/-Fontal statement-/
A-Formal statement-/ theores amc12b_2022 2tte:222221____iii__eee. _a_nm_sfff____ (s: (o
thecren amc12b_202 2tt.:o.o2000000mtt11e3e...
theores wxc12b_2021, 20_____000_____1122222___.3 (x:
(x:
Dig : 1/(1 (2 x 144 53):
Oio :2 1/(1 12 23 144 53)):
144 :3):
x=3/4:bby
x=3/4=bby
3-3/4 3/34
corxy
dorry
5
sorry
Figure 2: Correction example of amcclbb20022 problem in miniF2F across versions 2s and 2c.
2.1 Errors in informal statements
Incomplete statements. There are problems that not provide enough information or do not mention the type of variables. There are also instances where the informal statement differs from the original problem statement presented in the competitions such as IMO. all such cases, we use original informal statements.
Unprovable problems. These of problems miss critical hypotheses to prove the goal; therefore. making them unprovable.
Multiple choices in the statement. In miniF2F-v2s, we filtered the informal statements from multiple choice style answers to reflect only the final goal to be proved. In miniF2F-v2c, we added all the choices the formal statements. Figure 2 illustrates answer from the informal statement so that matches the original AMC statement, and introduce the multiple-choice options in the formal statement. In v2s, we omit the multiple-choice options from the informal description so that it matches the formal statement leading to simplified problem where the solution known. Additional examples can be found in the Appendix.
example. In v2c, remove the correct
Wrong given solution. Another subset of incorrect informal statements provide a wrong or inconsis- tent solution that deviates from the original problem statement and solution.
No given solution. Some of the informal statements do not provide solution after the problem description, yet the formal statements contain the solution. For miniF2F-v2s, we add the solution to informal statements. For FFv222 we remove the solution from the formal statement and provide sorry for the ATP model to find and prove.
2.2 Errors in formal statements
Excessively simplifying the problem by changing the goals or changing the conditions. This subset of problems aim to prove simpler goals compared to the original informal description. These problems do not reflect the original difficulty of the problem; therefore, making the LLM's task casier. We segregate these problems into two categories: simplified and excessively simplified. The common culprits behind simplification are omitting part the informal statement, simplifying the goals, adding helpful assumptions, wrong type declarations (e.g., proving goal for non-negative real numbers instead of all real numbers, or using equivalences instead of functions). Excessive simplification cases those where the goal is significantly altered.
Not using the correct functions/expressions declaration of functions and expressions. In some cases, informal statements describe conditions, functions, etc, whereas the formalized version does not declare them. We fix these inconsistencies in revised versions of miniF2F.
Lean. Another subset of formal errors are incorrect

---

Table 1: Comparison of effective accuracy across different autoformalizers and theorem provers. Effective accuracy refers to final accuracy after autoformalizer formalizes the problem statements and theorem prover attempts to prove them. Experiments are performed with @ 128 for translators and @32 for theorem provers. Numbers in blue are gains in accuracy as result of higher quality benchmark. Numbers red are drop aceuracy as a result of increased difficulty compared the simplified problems in miniF2F-v1.
Verification
miniF2F
Theorem prover accuracy (%)
Setting
excessively simplified proofs
Deepseek- Prover-
Goedel- Prover-
Kimina-
DeepSeek-
split
Goedel- V2-7B
Prover- Distill-7B
Prover-
VI.5-RI.
SFT
V2-7B
vl
34.4
37.7
41.0
50.8
54.1
test
full score
v2s
34.0 (-0.4)
37.7 (0)
42.2 (+1.2)
47.5 (+3.3)
53.3 (-0.8)
Herald translator
v2c
33.2 (-1.2)
36.9 (-0.8)
39.3 (-1.)
43.4 (-7.4)
48.4 (-5.7)
v1
no score (Olympiad setting
21.7
24.2
27.5
33.2
36.9
v2s
test
31.1 (+9.4)
34.8 (+10.6)
38.9 (+11.4)
44.7 (+11.5)
50.0 (+13.1)
v2c
30.3 (48.6)
34.0 (49.8
36.5 (49.0)
40.6 (47.4)
44.7 (47.8)
vl
43.0
47.1
50.0
62.7
64.3
valid
full score
v2s
43.0 (0)
46.3 (-0.8
50.0 (0)
58.6 (-411)
59.4 (-4.9)
v2c
41.4 (.1.6)
43.4 (3377
46.3 (3.7)
52.9 (-9.8
53.3 (-11)
v1
no score (Olympiad
31.6
34.4
36.9
44.7
46.7
valid
v2s
40.2 (48.6)
43.4 (+10)
47.1 (+10.2)
55.7 (+11)
56.1 (+9.4)
setting)
v2c
38.5 (46.9)
40.6 (46.2)
43.4 (46.5)
50.0 (45.3)
51.2 (44.5)
vl
42.2
48.0
60.2
69.7
77.5
Kimina autoformalizer
v2s
test
full score
43.9 (+1.7)
47.6 (.0.4)
62.3 (+2.1)
63.5 (46.2)
74.2 (3.3)
v2c
40.6
46.7 (.1.3)
56.1 (4.1)
55.7 (-14)
65.6 (.11.9)
vl
no score (Olympiad
24.2
27.9
35.2
40.2
49.2
v2s
test
41.8 (+17.6)
47.5 (+19.6)
58.6 (+23.4)
60.2 (+20)
69.7 (+20.5)
setting)
v2c
38.1 (+13.9)
44.3 (+16.4)
52.0 (+16.8)
52.5 (+12.3)
61.5 (+12.3)
v1
52.0
55.3
64.8
75.4
78.7
valid
full score
v2s
51.6 (-44)
52.8 (-2.5)
65.6 (40.8)
72.1 (-3.3)
74.6 (-4.1)
v2c
47.5 (-4.5)
52.0 (43.3)
60.7 (-4.1)
63.5 (-11.9)
66.4 (+12.3)
vl
no score (Olympiad setting)
38.1
40.6
46.7
51.2
54.9
valto
v2s
48.0 (49.9)
52.0 (+11.4)
61.1 (+14.4)
68.4 (+17.2)
70.1 (+15.2)
v2c
43.9 (45.8)
48.4 (47.)
56.6 (49.9)
60.2 (+9)
62.3 (47.4)
Unprovable statements. We identified total of 16 problems across test and validation sets that do not have solution in their current form, which a critical factor when comes to reliable evaluation of theorem provers. The errors come from improper translation of the informal statement formal counterpart, such as missing brackets or using a wrong function from the Mathlib library.
"I this setting. simplification is rewarded and encouraged. If LLM, proves excessively simplified modification of problem. it still gets full credit. This is the setting that perhaps inadvertently being used to evaluate accuracy of formal reasoning models.
'Each Olympiad, or competition, may have different rules on giving partial scores, and these rules might even change year by year. To make evaluation clear, opted for the choice of giving credit for excessively

---

Table 2: Comparison of autoformalization accuracy of Herald and Kimina translators at @ 128 between LLM and human evaluators. Back translation and LLM equivalence check pipeline is adopted from 14.
miniF2F-v1
miniF2F-v25
miniF2F-v2c
Translator
Evaluator
test
valid
test
valid
test
valid
Herald's automated judge
97.5%
97.1%
96.7%
97.5%
95.1%
97.1%
Herald
Human
62.7%
69.7%
66.0%
68.9%
54.1%
60.2%
Herald's automated judge Human
98.4%
98.4%
99.6%
98.8%
98.4%
98.8%
Kimina
90.6%
88.1%
91.0%
88.1%
75.4%
76.6%
3 Evaluation of complete formal reasoning pipelines starting from informal statements
This section presents our experiments with an end-to-end pipeline that aims to prove informal theo- rems with the aid of formal theorem prover systems. The setting is motivated by Math Olympiad-style problems, where the task is to produce a correct solution for given informal statement. We selected every original problem used to construct the miniF2F benchmark and employed them to evaluate how well state-of-the
autoformalizers can work with SoTA theorem provers.
For each problem we begin by feeding the informal statement to an autoformalizer; we keep the first formal output that both passes REPI. verification and remains semantically faithful to the source, which is judged by human experts. We then attempt to prove the resulting goal with several theorem provers, and finally we compare the derived theorem with the original problem, recording any discrepancies. We refer to final accuracy of autoformalizer and theorem prover collaboration as "effective accuracy"..
Table M summarizes our end-to-end results on miniF2F-vl and miniF2F-v2. For each pair of autoformalization and theorem provers, report two effective accuracy metrics: (i) the percentage of proofs that pass REPL verification giving credit to all proofs even for the ones that are excessively simplified compared to the original informal statements, and (ii) the percentage of proofs that both pass verification and align with the original problem statement, i.e., the Olympiad setting.
This table highlights the impact of having high quality and error-free benchmark where all the- orems are provable, and all the formal and informal statements match each other. For all pairs of autoformalizttion and theorem provers, effective accuracy is considerably higher on miniF2F-v2s and v2c compared to when the pair of models are evaluated in the "Olympiad setting". This gain in accuracy is despite the fact that v2 versions of miniF2F are more difficult. In the "full score" setting, however, where the LLMs get full credit for proving excessively simplified problems, the accuracy v2 versions of miniF2F are considerably lower. More detailed analysis of these results are explained the following sections where we evaluate the accuracy autoformalizers and thcorem provers separately each version of miniF2F.
Evaluation of autoformalization models
This section evaluates the performance of autoformalizers on miniF2F-v1, v2s and v2c. The most notable observation of this section is that the reported accuracy of autoformalization models in the literature are largely inflated as those evaluations are typically performed by LLMs. For example, when we perform human review of the outputs of Herald @ 128 that LLM has marked as 97% correct, we arrive at much lower accuracy of 66%. And the same observations hold for Kimina autoformalizer.
We consider two specialized autoformalization systems. Herald translator [1 and Kimina auto- formalizer [12), and one general- general-purpose purpose model, o4-mini [15]. All experiments use sampling budget of @ 128 for the dedicated autoformalizer models and @ 10 (with intermediate compiler
simplified proofs while giving full credit for the simplified proofs. In most Olympiads, an excessively simplified proof will get or close zero score.

---

Table Comparison of autoformalization accuracy of Herald translator, Kimina autoformalizer and 04 mini on the original version of miniF2F (miniF2F-v1) and miniF2F-v2. The o4-min translation has sample budget up to 10, but the generation stops at the first correctly compiled attempt, while other models are evaluated with @ 1.
miniF2F
Model Formalization Accuracy (%)
verified by
ver.
split
Herald translator
Kimina autoformalizer 04 mini*
v1
test LLM
49.6%
58.6%
vl
test human
55.3%
88. 1 1
46.3%
v2s
test LLM
49.2%
54.5%
v2s
test human
51.6%
79.5%
51.6%
v1 valid
LLM
51.2%
57.8%
v1
valid
human
59.4%
82.0%
47.1%
v2s
valid
LLM
50.4%
51.6%
v2s
valid
human
48.0%
78.7%
52.5%
feedback) for o4-mini. We note that although 04-mini has a different sample budget, we stop at the first successful compilation attempt, which puts it on par with @ Herald translator and Kimina autoformalizer models. We exclude any autoformalization outputs that fail to pass the Lean compiler to ensure syntax correctness. Lean compiler of choice Lean REPL [6].
To evaluate Herald translator, Gao et al. 14 used MeernL-M2--athhPluu--- 17 for back-translation and DeepSeek Chat v2.5 18 for equivalence verification. As observed by Ye al. [99] using an LLM as judge reduces verification overhead but can diverge from human judgments. In our experiments, we did not change mack-translation model; however we used Deepseek- V3 (20), instead of Deepseek-V2.5 for natural language validation. To present accurate results aligned with the human grasp of presented problems, we manually verified every translation and report both M-beeeed and human-verified accuracies. All human verifications were conducted by Lean experts. For the @ 128 setting, human evaluation is performed only on the first translation that successfully passes the Lean compiler, rather than on all 128 translations.
Table 2 compares the accuracy of the LLM evaluator with human verification both versions of minil 2F, using the Herald translator and Kimina autoformalizer with sampling budget of @ 128. The LLM tends to produce false positives and therefore reports much higher accuracy than human evaluator. In many cases, it treats small discrepancies between statements as negligible even though they significantly affect the meaning of the statements; as shown in Section 3 these differences accumulate and reduce the practicality of full anformal-to-formm pipelines. Consequently, autoformalizations should be evaluated with great care, and semantic alignment must remain strict.
To broaden our study, we conducted @ experiments with Herald translator, Kimina autoformalizer, and 04-mini. Here, the opposite pattern appears: the LLM evaluator assigns lower accuracies than the human evaluator. We hypothesize that with a larger sampling budget the LLM has a higher chance of hallucinating and assigning incorrect labels, whereas @ 1 behaves more conservatively. Moreover, while human evaluation at @ 128 shows only a 10-15% improvement over @ 1, the LLM evaluation suggests almost double the gains.
Kimina Autoformalizer attains higher accuracy than Herald Translator under both LLM-based and human verification, with accuracies ranging from 78% to 88% across both versions of miniF2R. However, when evaluating on miniF2F-v1 against miniF2F-v2, both Herald Translator and Kimina Autoformalizer exhibit performance decline, whereas o4-mini improves the corrected dataset. This finding suggests that current autoformalizers may suffer from data contamination.
We also present the failure modes of each autoformalization model by topic in Appendix [ This analysis highlights the types of mathematical domains where current autoformalizers struggle the most, providing guidance for future works.
5 Evaluation of theorem provers on formal statements
In this section we conduct a series of experiments only with whole-proof generation L.MSs starting from the formal statements in the miniF2F-v1, v2s, and v2c. This is to provide insights about the
7

---

Table 4: Comparison of whole-proof generation models' accuracy on the original version of miniF2F and miniF2F-vv.
DeepSeek- Prover- V2-7B
Deepseek- Prover-
Prrvee---Prover-
Goedel-Prover- SFT
Pronin- Distill-7B
Goedel- V2
Dataset
V1.5-RL
vl-test
50.0%
58.2%
65.2%
73.4%
82.0%
v2s-test
41.0%
48.4%
59.0%
68. %
74.2%
v2c-test
38.1 %
46.3%
57.0%
64.4%
72.5%
vl-valid 63.9%
68.9%
73.0%
79.4%
83.6%
v2s-valid
55.3%
59.8%
68.0%
73.4%
77.9%
v2c-valid
52.0%
57.8%
67.6%
70.5%
73.4%
Table 5: Comparison of whole-proof generation models' accuracy the subset of problems in miniF2F-v2 that were previously unprovable on the original version of miniF2R.
Goedel-
Kimina-
Deepseek-
Propseek-Prover VI.5-RI.
Goedel- V2
Unprovable subset
Prover-
Prover-
Prover-
SFT
Distill-7B
V2-7B
miniF2ffv22-test (out of 13)
(30.8%)
(30.8%)
5 (38.5%)
(38.5%)
(61.5%)
miniF2f-v2s-valie (out of 3)
(33.3%)
(33.3%)
1 (33.3%)
(33.3%)
(33.3%)
differences in the formal statements of the two versions of miniF2F while ablating the effect of autoformalizers. Following the literature, we use a sampling budget of @32 all runs. Deepseek- Prover-VI.5-PP (21), Goedel-Prover-SFT [22] and Seepseek-Prover-VVe V2-7B [23] are evaluated under
Lean v4. 9. o, matching the versions used in their original papers, whereas Kimina-Prove Distill- 7B 12 is tested with the newer Lean v4. 14.17.60 O. All experiments were performed eight NVIDIA A5000 GPUs with 128 CPU cores.
Performance of theorem provers on miniF2F-v2. Table reports the accuracy of selected theorem provers on miniF2F-v1, v2s, and v2c. Notably, the accuracy of every theorem prover is lower on miniF2F-v2, since many simplifications made in miniF2F were reverted back, and theorems became more challenging. The proposed dataset poses a greater challenge state-of-the- -ortt---rtttttttt LLMs. We observe that increased difficulty of v2c leads to 11.2% drop in accuracy for Deepseck-Prover- V2-7B, and many failure cases come from Math Olympiad level problems that are especially hard to prove.
Performance of theorem provers on the modified problems in miniF2F-v2. Although the overall accuracy declines on miniF2F-v2, is important note that this version corrects sixteen statements that were unprovable in the original benchmark. All theorem provers can now solve subset of these repaired problems, which raises their accuracy on this specific group of tasks. The results are reported
Table 6: Comparison of whole-proof generation models' accuracy on the subset of problems in Fini that were simplified in the original version of miniF2F
Goedel- Prover- SFT
Kimina-
Deepseek- Prover-
Deepseek-Pree Prover-
Goedel- V2
Simplified subset
Prover-
V1.5-RL
Distill-7B
V2-7B
miniF2F-v1-tes. (out of 40) miniF2ffv22stest
29 (72.5%)
30 (75.0%)
31 (77.5%)
36 (90.0%)
37 (92.5%)
23 (57.5%)
24 (60.0%)
25 (62.5%)
29 (72.5%)
33 (82.5%)
(out of 40)
ninil (out of 48)
27 (56.2%)
29 (60.4%)
30 (62.5%)
34 (70.8%)
38 (79.2%)
miniF21-v2s-valit (out of 48)
25 (52.1%)
25 (52.1%
27 (56.2%)
31 (64.6%)
35 (72.9%

---

Table 7: Comparison of whole-proof generation models' accuracy on the subset of problems in miniF2F-v2 that were excessively simplified in the original version of miniF2F.
Goedel-
Kimina-
Deepseek-
Excessively Simplified subset
Deepseek- Prover-
Goedel- V2
Prover- SFT
Prover- Distill-7B
Prover-
V1.5-RL
V2-7B
miniF2F-v 1-testt
21 (46.7%)
33 (73.3%)
33 (73.3%)
37 (82.2%)
42 (93.3%)
(out of 45)
miniF2f-v2s-test
10 (22.2%)
13 (28.9%)
24 (53.3%)
27 (60.0%)
36 (80.0%)
(out of 45)
miniF2F-v1-valle (out of 36)
26 (72.2%)
26 (72.2%)
28 (77.8%)
29 (80.6%)
31 (86.1%)
minif2f-v2s-valid
7 (19.4%)
(25.0%)
17 (47.2%)
17 (47.2%)
19 (52.8%)
(out of 36)
in Table Since we provide the formal proofs for all problems in miniF2F-v2, one can be sure that all theorems are provable.
To further assess the impact of our revisions, compare prover accuracy the previously defined simplified and excessively simplified subsets. Table shows that theorems in the simplified group pose only modest challenge: accuracy falls for every model, yielding a 15-18 % drop on the set, while the validation set experiences an even smaller decline. The picture changes significantly for the excessively simplified subset. Here, every model struggles: test-set accuracy decreases by more than 20%, and the validation set loses over 30%. Deepseek- Pronek---Poo-VV--eee V1.5-RL and Goedel- Sooede--rrver-SS SFF suffer the largest losses, in some cases up to 40-50% In contrast, Kimina-Prov Prover-Distill-- comparatively robust, proving 53.3% of the test problems and 47.2% of the validation problems, indicating strong generalization. Deepseek- Provee-- V2-7B also struggles with more challenging counterparts and exhibits 22.2% drop in test set and 33.4% drop in validation set. By making the subset of problems closer to the intended difficulty, we see that each LLM struggles least with some of the new theorems. This indicates the importance of the renewed version of miniF2F with scaled difficulty.
remains
Related Works
Autonomous AI systems excelling in reasoning and scientific discovery. With the rise generative models, we have seen their success in scientific discoveries (24). For example, FunSearch (25 succeeded writing bin-packing algorithm that is faster than any human written algorithm. These systems, usually consisting LLM their core, have shown remarkable ability in automated reasoning. For example, AlphaGeometry (26) was able to reach gold-medal level in solving geometry problems at IMO. AlphaProof [10], similarly reached melver-medal level in proving IMO problems in number theory and algebra. Other examples include AlphaCode (27 and AlphaEvolve (28
Silver and Sutton [29] suggest that we will see a new generation of Al agents that will reach unprecedented abilities predominantly by learning from experience. This argument largely draws not just from recent successes of Al systems. but also looks back at the successes of systems such as AlphaGo which was able to learn the game of Go merely by playing with an automated adversary, and ultimately reaching the level of expertise to beat the human champion. When the same algorithm was transformed to play the Japanese chess, it also passed the best human performance while the model developers had no familiarity with the Japanese chess. Indeed, the strategies utilized by the model were known to fail by human champions, yet the models devised them in ways that were able to beat those same champions.
The idea here is that to make new discoveries or to arrive at models that can find better ways of playing a game or can excel at proving mathematical theorems, the models have to be given the space to explore the possibilities by themselves with no or minimal human intervention. From this perspective, fully automated pipeline for mathematical reasoning would be preferable to a pipeline that needs human in the loop for formalization, etc. Hence, in this work, we suggest fully automated pipeline to evaluate AI systems for formal reasoning.

---

Automated Theorem Proving, Automatically proving mathematical theorems has a rich history including SAT and SMT solvers. In recent years, LLMs have shown a remarkable capability to generate formal proofs by themselves 330 30
32
33
34
12 or with help from other automated
10 [9]. Before the release of Kimina Prover, SoTA LLMs on the task of theorem proving were only able to prove theorems with relatively short proof' in formal language [40], heavily relying on automated solvers in Lean such as nlinarith. The longest proof written by Goedel Prover miniF2F consisted of ~ 10 lines. Kimina Prover, however, increased this limit to a few hundred lines using a longer context length.
systems such as retrieval-based and/or search methods R5
Autoformalization. This can be viewed as a translation task 41 42 where statements from informal language are translated to the language of a formal verification system such as Lean. Informalization is the reverse translation from formal language to an informal one which is considered an easier task, L.LMs have shown a remarkable ability in translation tasks especially when large corpus of text are available in two or more languages. Similarly LLMs are good at writing code in languages such as Python and C++ 45
We also have seen gradual improvements in the accuracy of LLMs in
autoformalization
Herald [4] the current state-of-the-ard in the literature, reports an accuracy of 97% on the mF while its accuracy is measured by an LLM and not verified by a human familiar with Lean. There are generally two difficulties in the field of autoformalization. First, high quality data paired in formal and informal languages is scarce. Second, there are no automated systems that can reliably verify the correctness of translation 44 and as we will see. LLMs may not be reliable in evaluating whether translation is correct. Even when the ground truth is available in formal language, it may not be easy, for human nor a L.LM, to evaluate whether a freshly generated formal statement is equivalent to the ground truth. There has been considerabe work in this domain trying to automate the evaluation of equivalent formal statements 45 46).
Benchmarks for formal reasoning, Over the past few years, the community has introduced several mataammmateematics benchmarks of varying difficulty. ProofNet 47 focuses on undergraduate- level mathematics, while PutnamBench [48 collects problems from the William Lowell Putnam Competition (1962-2023). NuminaMath [49] and miniCTX (50) target advanced theorems drawn from Lean projects and textbooks. Recently proposed, Con-NF 44 is specifically designed for an autoformalization task. this work, we concentrate on the Fi dataset (51), which consists of 488 problems sourced from texthooks and competitions such as IMO, AIME, and AMC.
Reliability of mathematical benchmarks. Ensuring the reliability of LLM benchmarks is a critical concern for the research community. To accurately assess model capabilities, benchmarks must be both comprehensive and error-free. Vendrow al. (52) evaluated numerous datasets across various tasks and introduced the concept of platinum benchmarks, i.e. those containing minimal errors and verified by human experts. The integrity of these benchmarks essential for measuring progress in formal reasoning. Accordingly, we dedicate our efforts to exhaustively verify the miniF2F dataset.
7 Limitations
This work only covers Lean language, even though mini is available for other languages, too. Our corrections to the informal statements are applicable to all users of miniF2F.
8
Conclusion
We introduced miniF2F-v2, a revised version of the miniF2F benchmark. Hundreds of theorems were re-verified and changed to match the difficulty of their source problems, and the sixteen unprovable statements in the original dataset were fixed. To recreate a realistic setting of math Olympiad competitions, using the SoTA models in the literature, we built a completely automated pipeline of theorem proving starting from natural language statements. Our evaluation results show that in such setting the accuracy of current models will significantly drop on miniF2F-v1. However, when we do the same evaluation on miniF2F-v2, some of the lost accuracy is gained back because of the higher quality of the revised dataset. We further compared LLM evaluation of the outputs of autoformalization models with expert human verification and observed substantial gap: LLMS marked many formalizations as correct even though they differed from the intended statements. By our evaluation, the accuracy of SoTA autoformalization model on miniF2F-v1 is 66%, not the reported 97%. We hope that miniF2F-v2 will serve as a clearer and more demanding benchmark and will guide future progress in both autoformalization and formal theorem proving.
10

---

Acknowledgments
The work of Farzan Farnia is partially supported by a grant from the Research Grants Council of the Hong Kong Special Administrative Region, China, Project 14209920, and is partially supported by CUHK Direct Research Grants with CUHK Project No. 4055164 and 4937054. The authors also thank the anonymous reviewers for their helpful feedback and constructive suggestions.
References
[1] Alan M Turing. Intelligent machinery, a heretical theory. Philosophia Mathematica, 4(3), 1948.
[2] Bruce Pandolfini.
Kasparov and Deep Blue: The historic chess match between man and machine. Simon and Schuster, 1997.
[3] David Silver, Julian Schrittwicser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, al. Mastering the game of Go without human knowledge. Nature, 550(7676):3543355 359, 2017.
[4] Stanislas Polu and Ila Sutskever. Generative language modeling for automated theorem proving. arXiv preprint 2tti::20000033393 2020.
[5] Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, page 625-635, Berlin, Heidelberg, 2021. Apringer-Verlage
[6] Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants, In International Conference on Machine Learning, pages 6994. PMLR, 2019.
[7] Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier AI. In Proceedings of the International Conference Machine Learning, 2025.
[8] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu, miniF2F: A cross-system benchmark for formal Olympiad-level mathematics. International Conference on Learning Representations, 2021.
[9] The AIMO Prize: Airtificial Intelligence Mathematical Olympiad. https://aimoppiie..omm//
[10] Google DeepMind. achieves silver-medal standard solving international math- ematical olympiad problems.
https://deepm:: google//iscover/bllg
ai-solves- imo-
-eee--imoo-roooeeeee problems at medalver-mddallleeeeee 2024. Accessed: 2025-05-
088.
[11] Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35, 2022.
[12] Haiming Wang, Ment Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying. Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schmidt, Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang, Stanislas Polu, Thibaut Barroyer, Wen-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang, Zhilin Yang, Zhengying Liu, and Jia Li. Kimina-Prover Preview: Towards large formal reasoning models with reinforcement learning. 2025.
[13] Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yu Chen, Yuntian Liu, Yang Jiao, and Tao Luo. Atlas: Autoformalizing theorems through lifting, augmentation, and synthesis of data, 2025.

---

[14] Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated lean 4 dataset. In The Thirteenth International Conference on Learning Representations, 2025.
[15] OpenAI.
Introducing openai 03 and 04-mini.
https:///genaai.com/innee
introducing-ee and 04-mini/ April 2025.
[16]
Lean FRO. A cead-eval-print-lon leanprover community/rep: 2023.
for Lean 4.
https://github. com/
[17]
Huaiyuan Ying. Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, Yudong Wang. Zijian Wu, Shuaibin Li, Fengzhe Zhou, Hongwei Liu, Songyang Zhang, Wenwei Zhang, Hang Yan, Xipeng Qiu, Jiayu Wang, Kai Chen, and Dahua Lin. Internlm-math Open math large language models toward verifiable reasoning, 2024.
[18] DeepSeek-AI. AL. Deepseek-v2: A strong, economical, and efficient mixture-ooe cacttuue--ff-epeee of-experts language model. 2024.
[19] Jiayi Ye, Yanbo Wang, Yue Huang, Dongping Chen, Qihui Zhang, Nuno Moniz, Tian Gao, Werner Geyer, Chao Huang, Pin- Chen, Nitesh Chawla, and Xiangliang Zhang. Justice or prejudice? quantifying biases in LLMM-ss-ajuudee In The Thirteenth International Conference on Learning Representations, 2025.
[20] DeepSeek-AI. Deepseck-v3 technical report, 2024.
[21] Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang. Xuan Lu, Qiushi Du, et al. Deepseck-prover-ve Harnessing proof assistant feed- back for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.088) 08152, 2024.
[22] Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-Prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07644. 2025.
[23] Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu. Wenjun Gao, Daya Guo, and Chong Ruan. Deepseck-prover--22 v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition, 2025.
[24] Hanchen Wang, Tianfan Fu, Yuanqi Du, Wenhao Gao, Kexin Huang, Ziming Liu, Payal Chandak, Shengchao Liu, Peter Van Katwyk, Andreea Deac, et al. Scientific discovery in the age of artificial intelligence. Nature, 620(7972):47-60) 2023.
[25] Bernardino Romera- Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M Pawan Kumar, Emilien Dupont, Francisco JR Ruiz, Jordan S Ellenberg, Pengming Wang, Omar Fawzi, et al. Mathematical discoveries from program search with large language models. Nature, pages 1-3, 2023.
[26] Trieu H Trinh, Yuhuai Wu, Quoe V Le, He He, and Thang Luong. Solving Olympiad geometry without human demonstrations. Nature, 625(7995):476 482, 2024.
[27] Yujia Li, David Choi, Junyoung Chung, Nate Kushman, Julian Schrittwieser, Rémi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago, et al. Competition-level code generation with Alphacode. Science, 37866624)11022-1097 2022.
(28) Can Cui, Wei Wang, Meihui Zhang. Gang Chen, Zhaojing Luo, and Beng Chin Ooi. Alphae- volve: A learning framework to discover novel alphas in quantitative investment. In Proceedings of the 2021 International conference on management of data, pages 2208-22282222222 2216, 2021.
[29] David Silver and Richard S Sutton. Welcome to the era of experience. Google AI, 2025.
12

---

[30] Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du Wenjun Gao. Qihao Zhu, Dejian Yang. Zhibin Gou, Z. Wu, Fuli Luo, and Chong Ruan. peepseek-prover-vv 1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search, 2024.
[31] Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang. Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-Prover: frontier model for open-source automated theorem proving, 2025.
[32] Jingyuan Zhang, Qi Wang. Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, and Kun Gai. Leanabell-Prover: Posttraining scaling in formal reasoning, 2025.
[33] Kefan Dong and Tengyu Ma. STP: Self-play L.M theorem provers with iterative conjecturing and proving. arXiv preprint wrwiv:2502.002//1 2025.
[34] Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying. Jiayu Wang, Dahua Lin, and Kai Chen. Internlm2.5-steeprrveer Advancing automated theorem proving via expert iteration on large-scale lean problems, 2024.
[35] Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning, 2022.
[36] Ran Xin. Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao. Yifan Sun, Shen Zheng, and Kai Shen. BFS-Prover: Scalable best-first tree search for Ilm-based automatic theorem proving, 2025.
[37] Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. Hypertree proof search for neural theorem proving. In Proceedings of the 36th International Conference on Neural Information Processing Systems, pages 26337-26349, 2022.
[38] Haiming Wang et al. DT-Solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In Proceedings of the ól Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Pupers), pages 12632-12646, 2023.
[39] 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, 2025.
[40] Roozbeh Yousefzadeh, Xuenan Cao, and Azim Ospanov. A Lean dataset for International Math Olympiad: Small steps towards writing math proofs for hard problems. Transactions on Machine Learning Research, 2025.
[41] Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. Intelligent Computer Mathematics; 11th International Conference, pages 255-270. Springer, 2018.
[42] Christian Szegedy. A promising path towards autoformalization and general artificial intel- ligence. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings 13, pages 3-20. Springer, 2020.
[43] Jiawei Liu, Chunqiu Steven Xia, Yuyao Wang, and Lingming Zhang. Is your code generated by chatgpt really correct? rigorous evaluation of large language models for code generation. Advances in Neural Information Processing Systems, 36:21558-215777 2023.
[44] Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, and Junchi Yan. Rethinking and improving autoformalization: towards faithful metric and a dependency retrieval-based approach. In The Thirteenth International Conference on Learning Representations, 2025.
[45] Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, and Xiaoxing Ma. Autoformalize mathematical statements by symbolic equivalence and semantic consistency. In The Thirty-eight Annual Conference on Neural Information Processing Systems, 2024.
13

---

[46] Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Autoformalizing euclidean geometry. In Forty-first International Conference on Machine Learning, 2024.
[47] Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. ProofNet: Autoformalizing and formally proving undergraduate--evel mathematics. arXiv preprint arXiv:2330. 2023.
[48] George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnam Bench: Evaluating neural theorem-provee the Putnam mathematical competition. In The Thirty-eight Conference Neural Information Processing Systems Datasets and Benchmarks Track, 2024.
[49] Jia Li, Edward Beeching. Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Costa Huang. Kashif Rasul, Longhui Yu. Albert Jiang, Ziju Shen, Zihan Qin, Bin Dong, Li Zhou, Yann Fleureau, Guillaume Lample. and Stanislas Polu. Numina- math. https: httpp::/giiti //github.. com/project, natetenumiin///aaa prttoo-proorsspppppe pwwpp/blob/maiin Eeport/numines dataset. pdf 2024. GitHub repository.
[50] Jiewen Hu, Thomas Zhu, and Sean Welleck. miniCTX: Neural theorem proving with (long-)
contexts. The Thirteenth International Conference on Learning Representations. 2025.
[51] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: a cross-system benchmark for formal Olympiad-level mathematics, 2022.
[52] Joshua Vendrow, Edward Vendrow, Sara Beery, and Aleksander Madry. Large language model benchmarks do not test reliability. In NeurIPS Safe Generative Al Workshop 2024, 2024.
[53] Timnit Gebru, Jamie Morgenstern, Briana Vecchione, Jennifer Wortman Vaughan, Hanna Wallach, Hal Daumé III, and Kate Crawford. Datasheets for datasets. Communications of the ACM, 64(11))86 92, 2021.
[54] Keiran Paster, Marco Dos Santos, Zhangir Azerbayev, and Jimmy Ba. OpenWebMath: An open dataset of high-quality mathematical web text. In The Twelfth International Conference on Learning Representations, 2023.
14

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: The paper presents a revised version of miniF2F benchmark as well as sys- tematic study of available autoformalization and theorem proving models. Main claims are supported by experimental results across different models and evaluation methods, e.g. human verification against LLM verification.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made the paper and important assumptions and limitations. A No or NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
It is fine to include aspirational goals as motivation as long as is clear that these goals attained by the paper.
2. Limitations
Question:
Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification: Yes, discuss limitations of the proposed benchmark in the main text.
Guidelines:
The answer NA means that the paper has limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create separate "I "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect the scope of the claims made, e.g., if the approach was only tested on a few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low or images are taken in low lighting. Or speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory assumptions and prool's
Question: For each theoretical result, does the paper provide the full of assumptions and complete (and correct) proof?
15

---

Answer: [NA]
Justification: The paper presents a new benchmark dataset, miniF2F-v2, and does not present discuss theoretical contributions.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross referenced.
All assumptions should be clearly stated or referenced the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but they appear in the supplemental material, the authors encouraged provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Question:
Answer: [Yes]
Justification: We disclose all sampling parameters, evaluation methods and Lean versions to reproduce all experimental results.
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution a specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way accomplish this, but reproducibility instructions for how to replicate the results, access to a hosted model (e.g.. in the case of large language model), releasing of a model checkpoint, other means that appropriate to the research performed.
also be provided via detailed
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how to reproduce that algorithm.
(b) the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is a new model (e.g., a large language model), then there should either way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reprodueibility may be tricky in some cases, in which authors are welcome to describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers have some path reproducing or verifying the results.
5. Open access to data and code
16

---

reproducible, they Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Question:
Answer: [Yes]
Justification:
We plan to release the proposed benchmark along with the proofs.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurlPS code and data submission guidelines (https://nips.co cc/
for more details.
While we encourage the release of code and data, we understand that this might not be possible, "No" is acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https /nips
for more details.
The authors should provide instructions on data access and preparation, including how access the raw data, preprocessed data, intermediate data, and generated data,
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended to the paper) recommended, but including URLs to data and code is permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: We report all hyperparameters and Lean versions required to reproduce the results.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core the paper to a level of detail that is necessary appreciate the results and make sense of them.
The full details can be provided either with the code, appendix, or as supplemental material.
7. Experiment statistical significance
Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer: [Yes]
Justification: We adopt the standard ATP practice of issuing multiple prompts LLM and considering a proof successful if any generated attempt passes the formal verifier. This repetition mitigates LLM's inherent variability, since verification systems can unambiguously confirm correctness.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by emor bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
17

---

The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
It should be clear whether the error bar is the standard deviation or the standard error of the mean.
is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out range (e.g. negative еπτог rates).
If error bars are reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information the com- puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification: We disclose resources used for experimental section in the main text.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate type of compute workers CPU or GPU, internal cluster, cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported the paper (e.g., preliminary or failed experiments that didn't make it into the paper).
9. Code of ethics
Question: Does the research conducted the paper conform, in every respect, with the NeurlPS Code of Ethics
Answer: [Yes]
Justification: The paper follows the code ethics and all generntelddowwllodde/sseed data has gone through sanity checks.
Guidelines:
The answer NA means that the authors have not reviewed the NeurlPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., there a special consid- eration due to laws or regulations in their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [NA]
Justification: The work proposes a new formal theorem proving/antffommaiizatoo bench- mark. We do not explicitly address societal impacts.
Guidelines:
The answer NA means that there is no societal impact of the work performed.
18

---

If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification: We will release the benchmark along with the proofs for the problems. We do not foresee risk associated with this benchmark.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model. for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
recognize that providing effective safeguards challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Justification: We cite and refer to every existing model and dataset used in this paper throughout the main text and appendix.
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset is used and, if possible, include URL.
The name of the license (c.g., CC-BY 4.0) should be included for each asset.
19

---

For scraped data from a particular source (e.g., website). the copyright and terms of service of that souree should be provided.
assets are released, the license, copyright information, and terms use in the package should be provided. For popular datasets, paperssi thood cww datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
If this information is not available online, the authors encouraged to reach out to the asset's 's creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
Justification:
The documentation will be provided alongside the benchmark dataset and proofs.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/model part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset is used.
At submission time, remember anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification: This paper does not conduct crowdsourcing research.
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According to the NeurlPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification:
The paper does not involve results related to human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with human subjects.
20

---

Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if' applicable), such as the institution conducting the review.
16. Declaration of LLM usage
Does the paper describe the usage of LLMs if is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, or formatting purposes and does not impact the core methodology, scientific rigorousness, originality of the research, declaration is not required.
Question:
Answer: [Yes]
Justification: We use LLMs to evaluate our benchmark on a variety of theorem provers and autoformalization models. Moreover, we compare the accuracy and performance of LLM-based evaluators for informal-to-forma. translation tasks.
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs as any important, original, or non-standard components.
Please refer to our LLM policy for what should or should not be described.
21

---

A Datasheet
Following the framework of 53 and [4] Table provides the additional information about our dataset.
Table Datasheet for our dataset
Questions
Answers
Motivation
For what purpose was the dataset created?
To correct uncovered errors and inconsistencies within miniF2F dataset [8] and to further facili- tate challenging benchmark for LLM--ased theorem provers and autoformalization models.
Who created the dataset and behalf of which entity?
The authors of this paper.
Who funded the creation of the dataset?
The company where the authors work. None.
Any other comment?
Composition
What do the instances that comprise the dataset represent?
miniF2F theorems, each consisting of 4 compo- nents: informal statement and informal proofs in English, formal statements and formal proofs Lean 4.
How many instances are there in total?
488 theorems
Does the dataset contain all possible instances or is it sample of instances from larger set?
Yes, we present all instances of the miniF2F dataset.
What data does each instance consist of?
formal theorem in Lean with its formal proof and its informal description and informal proof.
Is there a label or target associated with each instance?
Only informal prefix.
Is any information missing from individual in- stances?
No.
Are relationships between individual instances made explicit?
Not applicable.
Are there recommended data splits?
The dataset follows the same split as the orig- inal version, i.e. 244 test instances and 244 validation instances.
Are there any errors, sources of noise, or redun- dancies in the dataset?
No, there are no errors the proposed dataset to the best of our knowledge. Every formal statement and formal proof compiles with no error in I Lean4. All the informal statements and proofs are checked by human.
Is the dataset self-contained, does it link to or otherwise rely on external resources?
The dataset is self-contained corrected ver- sion of miniF2F.
Does the dataset contain data that might be considered confidential?
No.
Does the dataset contain data that, if viewed directly, might be offensive, insulting, threaten- ing, or might otherwise cause anxiety?
No.
Collection Process
Continued on next page
22

---

How was the data associated with each instance acquired?
All 488 instances originate from the miniF2F dataset and further augmented correct mis- takes and inconsistencies. Every theorem has corresponding entry in the source datasct.
What mechanisms procedures were used to collect the data?
The theorems were taken from miniF2F. Origi- nal problem statements were taken from official web pages of mathematical competitions such as IMO, AMC, AIME.
If the dataset is sample from larger set, what was the sampling strategy?
No. there is dataset and the original miniF2F dataset.
one match between this
Who was involved in the data collection pro-
The dataset was taken from open-source miniF2F dataset.
cess and how were they compensated?
Over what time frame the data collected?
Dataset was taken directly from miniF2F work.
Were any ethical review processes conducted?
No.
Was any prepocesiingcdlamigghbeinin of the data done?
Yes, we performed post processing of the dataset manually to uncover incorrect, mislead- ing, inconsistent or wrong statements.
Was the "raw" data saved in addition to the preprseesee/cleeeed/bbleeel data?
The raw data is open-source and available to the public.
Is the software that was used to preprocess/- clean/label the data available? Any other comments?
We used Lean compiler to type check the for- mal statements.
No.
Uses
Has the dataset been used for any tasks already?
We evaluated numerous theorem proving mod- els such Seepseek-Proved V1.5-RL, Goedel- Prover-SFT,
to evalu- ate the dataset. Additionally, we performed aut- oformalization experiments with Herald trans- lator, Kimina autoformalizer and OpenAI 04- mini models.
Is there a repository that links any all papers systems that use the dataset?
Public GitHub and HuggingFace links will be provided at later date.
What (other) tasks could the dataset be used for?
The dataset may be used for benchmarking theorem provers and autoformalization mod- els. Other tasks may involve incorporating the dataset into informal-formal theorem proving environments.
Is there anything about the composition of the dataset or the way it was collected and prepro- cessed/cleancc/labeeee that might impact future uses?
We do not anticipate future issues emerging from the proposed benchmark dataset.
Are there tasks for which the dataset should not be used?
The test set, and preferably validation set, should not be used to train the theorem provers and autoformalizers.
Any other comments?
No.
Distribution
Will the dataset be distributed to third parties outside of the entity on behalf of which the dataset was created?
Yes, we will release the dataset on public plat- forms such GitHub and HuggingFace at later date.
How will the dataset will be distributed?
GitHub, HuggingFace.
Continued on next page
23

---

When will the dataset be distributed?
The dataset will be distributed along with the camera-ready version of the submission.
Will the dataset be distributed under copyright or other intellectual property license, and/or under applicable terms of use?
Yes, the dataset will be released under the MIT license.
Have any third parties imposed IP-based or other restrictions the data associated with the instances?
No.
Do any export controls other regulatory re- strictions apply to the dataset or to individual instances?
No.
Any other comments?
No.
Maintenance
Who will be supportigghasting/aaiaaaannn the dataset?
The last author of the submission.
How can the owner/curator/manager of the dataset be contacted?
The manager of the dataset may be reached through an email or any other public means, such GitHub profile.
Is there an erratum?
Formal statements do not require erratum, and corrected informal statements are erratum of the original informal statements sourced from the miniF2F benchmark.
Will the dataset be updated?
Yes, we plan to periodically update the dataset versions of Lean become available.
the dataset relates to people, are there applica-
Not applicable.
ble limits the retention of the data associated with the instances?
Will older versions of the dataset continue to be supported/hostedmmaitaaiig
Yes.
If others want extend/augment/build on/con- tribute to the dataset, is there mechanism for them do so?
Yes. since we release coupled informal and for- mal statements, others may expand the dataset other formal languages, such as Isabelle. Informal statements can also be translated to other languages such as Chinese. The problems may be formalized further to cover more for- mal theorem proving languages.
Any other comments?
No.
24

---

B Effect of a clearly structured informal proof as opposed to a vague one
failure case of Kimina prover is aime saare__997_____ However, when we provide more clear informal proof for this theorem, Kimina Prover succeeds in proving it. This indicates the positive effect of better informal proof on the existing theorem provers, and the higher quality of miniF2F-v2.
aime_ ____1997_pppp __5 with informal proof'
miniF2F-v1
miniF2F-v2(s/e)
Find yx²y² i and y are integers such that y² yx² 30x 517. Show that it is 588.
Find 3x²y² if and are integers such that
y² - 3x. 30x 517. Show that yr is 588.
/-Formal Statement-/ theorem aime_ _ime_198__p5 (x y (ho 2 517)
(x
2)
30
3 (x 2 * y 2) 588 := by
sorry
Informal proof:
Informal proof:
If we move the x² term to the left side, it is [[SFFTifactorable]]]
From the equation y² + 3r²yy² 2 30x² 517 we first rewrite it as
(3x.2 + 1) 10) = 517 - 10
3 30x 517 -
507 is equal to 13 Since and y are inte- gers, 3x 11 cannot equal multiple of three. 169 doesn't work either, so 3z + 1 13,
Since squares are nonnegative this forces y² S 517, hence -22 S y S There are only finitely many integer choices for in this range, so we check each one: for each fixed y. the rewritten equation becomes con- crete quadratic in x which can be checked by direct computation yield 3x y 588. Thus in all cases the desired conclusion holds.
and x² 4. This leaves y² 10 39, so
y² = 49. Thus, yz²n²² = 3 x 49 588.
25

---

C Wrong formalization because of unfamiliarity with the mathematical definitions in Mathlib
Another failure case of Kimina Prover is algebra_cuurtrpplec onc.brrreg...................... leteee@@rrrerlloooere onrcubee5777 (algebra_55) 1_77 in short). The informal statement for this theorem relies upon simple definition of cube root common in precollege math. However, in Mathlib, the n root, via the rpow function, is defined using more advanced definition that is compatible with a broader network of definitions including the real roots of negative complex numbers and the continuity of roots of negative real numbers. The definition of nt root in Mathlib does not correspond to the common definition in precollege math, and therefore, the formalization of this problem miniF2F is wrong and unprovable. In other words, the rpow function in Mathlib is not equivalent to the definition of cube root as stated in the informal statement for this theorem and the use of rpow in this formalization makes this theorem unprovable in Lean.
In fact, we write a formal proof giving counterexample for the case when the variable is negative, proving that this theorem is unprovable in Lean as it appears in miniF2F-v1, i.e., a formal proof for unprovability of this theorem.
As alternative, in the below diagram, we show three correct formalizations of this problem. The first version still relies the definition of th root in Lean, but makes the variable nonnegative avoiding any conflict with lemma: Real.rpow def_o] __ff_________ of_neg in Mathlib. The second version defines new nh root function corresponding precollege math. The third formalization excludes the only possible negative root of equation hg- After correcting the formal statement, Kimina Prover successfully proves this theorem. The proofs of the correct formalization and the proof of counterexample for the incorrect statement in miniF2F wil released with the paper.
Informal Statement: Let r be a real number such that r + 1 3. Show that r 5778.
r3
Incorrect Formalization [miniF2F-v1]
Correct Formalization #1
theorem algebra5778 (r:
theorem algebra5778
R)
(ho (1/3:R) - (1/31/ = 3 7 1/13 5778 by
-
(ho : (1/3:B) + 1/1 = 33
(h1 0
73 + 1/r" = 5778 := by
Correct Formalization #2 [miniF2F-
Correct Formalization #3 theorem algebra5778
v2(s/c)]
theorem algebra5778
(r:R)
(r:R) (gpow R + Q + R)
(ho (1/3:3) + 11/3(1/3:R) =
(hq : qpow = fun x 1- x then
(h) r(1/3:)) + (1/2((-r)(/3B))
a.rpow(t a) else - (-Iz)rroww(1 a)) (hg : spowr (1/3) + 1/qpour (1/3) = 3)
3 + +/13/3= 5778 =578 by
3 1/13 = 5778 = by
D Examples of autoformalizer outputs on miniF2F v1 and v2
In this section, we present three examples of modified problems and analyze their impact on autofor- malization models. We show that supplying corrected miniF2F informal statements significantly affect model performance, and that the specific nature of each formalization error drives different model behaviors.
D.I mathd_ard aard__ageebr__00
The original informal statement mathd mathd_algebra___ allebra_333 omits several critical details and is defined ambiguously. In particular, it denotes a limit by "..." leaving the definition ambiguous. When tasked with this problem, both Herald and Kimina attempt encode the underlying recursive function explicitly, and fail.
26

---

To fix these issues, we provide a clearly specified version of the problem with an explicit recursive definition. After this revision, Kimina successfully produces correct autoformalization although Herald still fails. These results demonstrate that clearly written (i.e., higher quality) informal statements improves the reliability of autoformalization benchmarks, and can improve the accuracy of existing models, too.
D.2 imo_1960_p2
The original informal statement does not specify the solution to the question, i.e., the proof goal. In other words, the question asks the the examinees to first find the solution and then prove its correctness. With such an informal statement, autoformalization models should also leave the goal undefined using an additional sorry within the formal statement. This is what we do in our miniF2F-v2c. In miniF2F-v2s, however, we amend the informal statement with the answer so that it matches the formal statement. Clearly, the formal and informal statements in miniF2F-v2c are more difficult both for translation and for proving.
At the same time, with our modification of informal statement in miniF2F-v2s for this problem, both Herald and Kimina successfully produce correct formalizations. Although better informal-formal match increases the complexity for automated provers, our results demonstrate that faithful, detailed translations improve some autoformalization attempts.
Interestingly, since 04-mini is an advanced reasoning model, it automatically finds the solution for the statement in miniF2F-v2c and incorporates the answer the goal in its formal translation. This additional step that o4-mini takes, however, simplifies the problem along the way of translation and makes its formal proof much easier. This may may not be desirable in various contexts. As explained earlier in the paper, simplifying a problem during translation does not receive credit in our evaluation setting.
D.3 amc12b amc12b_2003_p3 2003_
In this example, the informal statement is correct. However, the formal statement is not a correct translation of it. The formal statement asks for extra solution, and drops the intricate detail of "a possible solution" " in the informal statement. This can be considered a mismatch between the informal and formal statements. Despite the fact that each of them is correct and provable, the formal and informal statements in the original miniF2F do not translate to each other. One possible approach is keep the correct informal statement and change the formal statement correspond which do in miniF2F-vve. In miniF2F-v2s, however, we chose to change the formal statement so that corresponds to the formal one. After this update, both Herald and 04-mini correctly autoformalize the problem in miniF2F-v2s. For miniF2F-v2c. we changed the formal statement to reflect the multiple-choice nature of the question. All options are equivalent except for the numerical solutions they correspond to. To preserve space, we replaced repeating blocks with "...". Only 04-mini was able to correctly autoformalize given statement.
27

---

Correction of mathd_at _aagebbrabbbb_33____ 31 with autoformalization outputs
miniF2F-v1
miniF2FFx22(sc)
Consider nonnegative real number and a recursive function from natural numbers real numbers. For all natural numbers, have u(n + 1) = /z: u(n). Assume that the as reaches infinity in its limit, u(n) goes to 9. What is the value of x? Show that it is 72.
V x + V +
find x.
Show that it is 72.
/-Formal statement-/
/-Formal statement-/
theorem mathd algebra_ei_ _1__iifff__fff
theorem Baahd_aagebba____ (osebra_31_minn _1__mmnifff_v
(x NNReal)
(x R) (hx
(u N + NNReal)
(u N RR)
(ho : V m, u (n 1)
(h. V n, (a 1) Real.sqrt
NNReal.sqrt (x n))
(x + n))
(hı Filter. Tendsto u
(h. Filter. Tendsto
Filter.atTop (nhds 9))
Filter.atTop (nhds 9))
NNReal. (x 9) : by
x 72 :- by
sorry
sorry
/-Kimina Formalized miniF2F-vi-/ theorem mathd_ alagddaaggbrraa31110
/KKimina Formalized miniF2F-v2s-/ theorem mathd algebra_33,_1__.. 3i_kiin
{x R}
(x R) (hx : S : R)) (hu : V u (n n))
(hx 0 < x)
sqrt (x
(h sqrt (x sxrt sqrt(x + sqrt(x sxrt(x + 0)))) 9)
(h Tendsto atTop (nhds 9))
72 :- by
by sorry
sorry
/-Herald Formalized miniF2F-vi-/ theorem mathd_algen aaapldd_ggbbba______ 31__eraldd sqrt (x sqrt (x + sqrt (x
/-Herald Formalized miniF2F-v2s-/
theorem mathd aadd__algbbaaa__ _1_braa______a he_ebaa_ herald (x
R) (h : 0 < x) (hx D' 1 : N,
sxrt(x 9)))) + x 72 by
(Real.sqrt (x (Real sqrt (x +
(Real.sqrt (x (Real sqrt (x
sorry
o))))>)))> 9)
72 by
sorry
/-o4mmini Formalized MinifFF-vv-/ theorem mathd_ algebra_3111.m.. taabbra_31_omiiii o4mini (x y R) (hi : y heal.sqrr (x +
/-o4-mini Formalized miniF2F-v2e
theorem mathd Bathhddalgbbaaa1_111 31_oimini {x
R} (h : 9 Real.sqrt (x + 9))
y)) (h2 = 9) 72 := by
x = 72 : by sorry
sorry
28

---

Correction of imo_ 10___960__p with autoformalization outputs
miniF2F-v1
miniF2FFvy2s
For what values of the variable does the following inequality hold:
Let æ be real number. Assume that:
+ 2z 0 (so that the square root is de- fined), (1 + 2x)² + 0 (so the de- nominator is nonzero), and 2x
4x
22x 1)2
< 2x ?
4x
(1=))+2a)
Prove that:
45 8
2 S x and I
/-Formal Statement-/
theorem imo 1960_p2 (x R) (ho 0 s 1 + x) (h) (1 Real. Real.sqrt (1
imo_1960_pp
x)) 2 # 0)
(h2 x / Real.sqrt
(1 2 x)) 2
-11
2) < x x 45 :- by
sorry
/-Kimina Formalized miniF2F-vi-/ theorem imo 1ttp_1960p2__iimmmm (x : R) (hx 0 0
/-Kimina Formalized miniP2F-v2s-/ theorem imo 1tt_196_pp2_kiminn (x R)
x
A sqrt
(hg : 1 2 * 2 0) (h, (1
(2 *
1) # 0)
Real.sqrt (1+ x)) 0)
(4 + - 2 / (1 sqrt (2
(h2
x-2 (1 Real.aqrt
1)) ~ 2 <
(1 2 x)) <
9)
V x > / 2) : by
-1 / 2 1 x A x < 45 := by
sorry
sorry
/-Herald Formalized vin-F/F-vi-/
/HHerldd Formalized miniF2F-vss- theorem imo ico_1960_pp2_hraal
theorem imo imo__960__ppp 11660__2_heealdd (x R) :
(x R)
(4
2 / (1 Real. sqrt (2 *
(hj 1 + 2 * 2 0) (h, (1
1)) ~ 2 < 2 9)
sqrt (1+ 2 x))
* 0)
by
(h;
x
Real.sqrt
sorry
(1 + 2 * x)) 2 < < * x 9)
-1 / 2 S A
< 45 / 8 : by
sorry
/-o4-mini Formalized miniF2F-vi-/
/-o4-mini Formalized miniF2F-v2s-/ theorem imo_1960_pp (x K))
theorem imo_ 1mo__160_pp2__00. _0mm_______mmii (x R)
(h_nonneg 2 1 0)
(h1
1 + 2
0)
(h_ne_zero
Real sgrt.sqrt..
(h2
(1 Real.sqrt
x))
x + 1) 0)
* 0)
* 2 (1 Real.squ sqrt (2 * +
(h3
4 * 2 (1 Real sqrt
1)) 2 *
(1 2 * x)) 2 < 2 * 9)
-1 / A 45 / A
-1 /
< 45 by
by
sorry
sorry
29

---

[Informal and Formal Mismatch] Comparison of amc12b 12b_ ae____03__________ across miniF2F-v1 and miniF2Fv2
miniF-FFvv
minil-2F-y2s
miniF2FFvve
The second and fourth terms of a geometric sequence are and Which of the follow- ing is a possible first term?
The second and fourth terms of a geometric sequence are and Show that the first term is either .23 or 2/3 3
The second and fourth terms of geometric sequence are 2 and 6. Which of the follow- ing is possible first term? Prove that it one of the fol- lowing options.
2v3
(A)
V3
(B)
2/3
(C)
v3
(D) v3
(E)
(A)
v3
(B)
3
Show that is (B)
(C)
(D)
v3
(E)
3
/-Formal Statement-i
f-Jocmal Statement-/
/-Fomaal Statement-i
thearex anc120,_n00 20000_2000____1____ (a (u:
theoren amc12b, wacc2i_2000__paee p0 (ax (u:
theorex axc12o, 2xct29_2003..6..c p2_
N
(3 (a:N 31 Ri
Ohg V a Bb :u ( Oug i. :0- 2/ aaallag -(2/ Roal. agrt 3)
(bo Y
==
(bg u. -)) ull 2/ Real aget - Beal 3)
Rual
-- 3
corzy
sorzy
3//
Beal.
sorry
(-iiminu Formalized 1-1 thearer 2rc122_20003.6. ktmmpp kimmin -+ () Dr. V., an=a0 (1a)
Formalized minif2F-22--/ theoren meoe12h__003.ppp pa.kii
i-Kimina Formalized miniF2F-v2o-/
theores axc125_2003, 2003__000_ppeee 1t...p6_.iiimm (a (bq:9 # tha
(uy o 0) (b] :a "r= 21
(al afg=
2) =0==22 =0==2""sgr33/33 3/3
r3= 6):
0h2 at 33 = 6 = 3
Roalaqrt am-- B0al.gqrt 3/3;=bb
==2"t asgrtt = 3==3:=by
corry
corzy
H-Herald Fonnalized miniF2F-y1-/ theorex anc12b_ 2003__6_bbeaa_.. :3) Ohg = ==3 A. a= -2* egrt 3/3 by norry
f-Horshi Formalizad miniF2F-atss.! theoren amc12b, 201222b22000ppppp 2000_p6..heaalle herald R)
H-Hemld Fonmalized miniF7F-yy2--4 theores nec122__000_____ (6 :) +r= t13
2
poal.grr 3/3 =/2 lgrl.agrt 3/3
a -Real.egrt V =2 Real Real.ggrt 3.V a -Raal agrt 3/3 a Beal aget. 3 Va 3--3-bbb
eorry
1-o4-mini mini Formalized minFFFF-yl- I-! theores 2002_66_0000e pe_iiii I # D 6Aa--2 aget 3/3.2
f-o4-mia Formolzzd- miniFIF-v2s-d
A-04-mini Formalized miniF2F-y2o- y2o-/ 2xc126__008 2euu:22__009_..eoo odaini
amci 2008_$000_________0_01000_______ _008__6_ooeiiii (hi:
=-2 Real agrt 3/3 -
a =
Bealaggt 3/3 :y
7 203 6
sorry
-Raalagrt agei
anget
Beal aget 3 3)
30

---

E Examples of modified statements
E.1 induectsouu.prrdpp/ooooooozz.//
The original problem was unprovable due to missing pair of parentheses, which led to an incorrect formalization. We corrected this error in miniF2F-v2 by inserting the appropriate parentheses.
E.2 _ime_1990_p4
In the original formal statement, three additional hypotheses (h1, h2, h2) explicitly assert that certain expressions are nonzero, which simplifies proof generation for theorem provers. These are extra assumptions that not present in the informal statement that given the participants of AIME 1990, and they are not necessary to prove the theorem. To remove this discrepancy between the formal and informal statements, the theorem more challenging for theorem provers as they have to prove each of those hypothesis as intermediate steps prove the theorem.
remove the added hypothesis from the formal statement. This makes
[Unprovable] Comparison of induction_ peldlplowe on2powklltoo2 across miniF2F-v] and miniF2Fv2
Show that for positive integer n, (I 1/2*)) < 5/22.
miniF2F-v1
minil:2F-v((see)
/-Formal Statement miniF2F-v1-/ theorem
/ /-Formal Statement miniF2F-v2-/ theorem
induction induction.porddpplonzee
pord1p1oon2ooklt5on2
induction induction.porddplonn2e pww.pppooooooooootttso
: N) (he : 0
(n N) (ho
n)
CI k in Finset Ice m, 1 + (1 2 k)
II k E Finset. Ice (1:1) n, ((1
2 by
R) (1 R) / 2 k)) (5
sorry
RD) by
sorry
[Simplified] Comparison of aime 1990 p4 across miniF2F-v1 and miniF2Fv2
Find the positive solution o 10r
0. Show that
29
10x
45
22-10z-68
miniF2F-v1
miniF2FFv2(s/e))
/-Formal Statement miniF2F-v1-1 theorem sime__1900_0
/-Formal Statement miniF2F-v2-/
theorem aime 1990_p4
(x R) (he 0
(x R) (ho
x)
(h1 x 2 10 * x
29 + 0)
(h4 1 / (x 2 10 * x 29)
(hæ
: 2 10
* I 45 7 0)
1 / (x 2 10
45) - 2
(hs
10
69 7 0)
(x 2 10
69)
0)
(h4 : 1 (x
10
29)
x
by
1 1 (x 2 10
45) 2 2
sorry
(x 2 - 10 * 69)
0)
13 : by
sorry
E.3 mmc12b_2021_pp
In this example, we retained each logarithm in its base form, writing log, a directly rather than converting it to log that the formal statement exactly corresponds to the informal one as it loge
31

---

appeared in the AMC. These changes yield slightly more challenging version of the problem. And V1.5-RL, we observe that all three theorem proving models, Deepseek-Prover Proeee---rov SreddelPrrvve-SPP and Kiminn-Prver-PPviixe-ssillll!
fail on the modified version of this theorem.
E.4 mathd_algebra_48
In the original miniF2F version, the problem was oversimplified: it introduced four variables (instead of two) and omitted the Euclidean-spaat space context, therefore providing extra hints that eases proof generation task for LLMs. In miniF2F-v2, we restore the two-variable formulation over RR remove these implicit assumptions. This leads to a spike in the problem's 's difficulty. These more faithful and challenging instances yield more rigorous benchmark for evaluating theorem provers.
32

---

[Simplified] Comparison of amc 1ic12b, __ across miniF2F-vv1 and miniF2Fv22
miniF2F-v1
miniF2FFy22
miniF2F-v2e
What is the value of log, 80
What is the value of log, logao 2
What the value of logg
Iog
logso 2
1og, 160 log20
logg 160
log, 160,
1og20
logza 2
Show that is 2.
Prove that it is one of the fol- lowing options.
(C) 5
(A)0
(B)1
4
(D)2
E log2 5
(A)0
(B)
(C)
Show that it is (D).
(D)2
(E) log2
/-Formal Statement
/-Formal Statement
/-Formal Statement
miniF2F-v1-/
miniF2F-v2s-/
miniF2F-v2c-/
theorem amc12b_ ccc12b__021_pp 2021__p9
theorem mac12b_2021.0
theorem amc12b_2021_p
Real.log 80
Real logb
(X
Real.log
(Real. logb 40 2)
(hX : X Real.logh
(Real. 2
Real. loab 2 160 /
80 / (Real.log] 40
Real. 1og 40)
Real. 20 2) 2
2) Real.logb 2
Real. log 160 /
:= by sorry
160 Real .lgbb
Real.log /
2) :
(Real.log 2
X 2 V X 4 v x
Real. log 20)
6 V X = 30 V X
by sorry
32 by
sorry
[Excessively Simplified] Comparison of mathd algebra 487 across miniF2F-vl and miniF2Fv2
What is the distance between the two intersections of = x22 and x + y = 1? Show that is V10.
miniF2F-vi
miniF2F-r2(s/e)
/-Formal Statement miniF2F-v1- v1-/ theorem mathd
/-Formal Statement miniF2F-ve
(a b Baailld_lgebr_eeee 487
theorem mathd_ aag.aaaggaaaaaa (F Set (BuclideanSpace
R) (ho : b a 2)
(h1 a + b = 1) (h2 : d = c
2)
(Fin 2)))
(hg + d = 1) (h4 a $ c)
(hF == {
x x1 (x 0) 2})
Real. sqrt ((a c)
(b
(hG G {x
x 1})
2) Real.sqrt 10 := by
I (F G))
sorry
(Fin 2)) (ho V E I + A V x B) dist Real sqrt 10
(A B EuclideanSpace
sorry
33

---

Examples of challenging miniF2F-v2e problems
F.1 1mo_1983_p6
In this problem, did not modify the informal statement; instead, corrected the paired formal statement. The original task is to prove an inequality and determine when equality occurs. vl, the formal statement reflects only the first part, omitting the statement and the proof of when the equality holds. We modified the given hypotheses to match the problem formulation, but one could argue that the original formulation also correct. More importantly, we ask the model perform two tasks: prove the inequality and determine the values of a, b, and to achieve equality, Now, when asked to saate-o-thh--
perform both tasks, the current medium-sizee and no longer produces a correct proof. We believe that the introduced changes are more faithful to the intended difficulty and reflect the limitations of current ATP models.
prover, Deepseek-Prone Prock--Prree-Y.e Pro--rr-o--77B fails
F.2 _90__997__p9
Another type of change made exclusively in miniF2F-v2c the correction of both informal and formal statements to match the intended difficulty. In vl, the immo_197__p problem statement is simplified and reworded to match the formal statement. Moreover, instead of requiring the prover to find the solution and prove it, the formal statement provides clear goal. We changed both the informal and formal statements to reflect the original imo 1997_ps pp formulation and tasked the models with coming up with the correct goal and writing valid proof. Our results suggest that when the goal is unknown, the models struggle to find valid proofs, since they essentially must solve two separate tasks achieve the result.
[Removed solution from formal statement] Comparison of imo_ 1eoo_193__pp_ across miniF2F-vi and miv2F2F-v2e
Let a, and be the lengths of the sides of a triangle. Prove that:
bbb(a - b) bRo(b c) + a) 0.
Determine when equality occurs.
miniF2F-v1
minil-2F-v2c
/-Formal Statement miniF2F-v1-/
/-Formal Statement miniF2F-v2- abbrev imo_1983_p66____m 1t__199_p6__ooution R R
theorem imo 1oo__983_pppp
(a
c R) (he 0
Prop := sorry
c)
(h1
a + b) (h2
b < c)
theorem imo 1m83_993_pp6 (T Affine Affine.Triangl. Triangle R
(ha
b c) : 0
2
b) 2 (b
(BuclideanSpace R (Fin 2)))
(c a) 1= by
a := dist (T.points 1) (T.points 2)
sorry
let b : dist (T.points 0) (T (T.ntints
2)
с :- dist (T (T.points 0) (T. po.points
1)
0 < a~2 * b * (a b) + b-2 * c (b
c) + c- * a * (c a)
(0 a-2
b) b-2
(b
c-
a)
1mo_1983__p_sooution a b c) := by
sorry
34

---

ISimplified informal and formal statements] Comparison of imo__997_ across miniF2F-v1 and miniF2F-v2c
miniF-2F-vl
minil:2F-v2c
Show that if x and y are positive integers such that z²² = yy" then (I, y) is equal to (1, 1), (16, 2), or (27.3).
Find pairs (a. of integers a, b 2 that satisfy the equation
/-Formal Statement miniF2F-vi-/
/-Formal Statement miniF2F-v2-/ abbrev imo_1997 -5__solution Set (NxN) sorry
theorem imo 10__1997_ppp
(x y N) (hn 0
y) (h1
y 2 y
(x, y) (1, 1) V (x, y) (16, 2) V
theorem imo 1mo_1997_p5
(x, y) (27, 3) by
(x N) (hg 1
sorry
y - y (x, y)
imo_ 10_11997_p5_oolutin0 := by
sorry
amc12_2000_p11
In our efforts make the problems closer Math Olympiad settings, removed the correct answers from MCQ-style questions and reformulated the goals to require first selecting the correct solution and then proving it.
[Omitted correct answers from multiple choice problems] Comparison of ame 12_2000 __p across miniF2F-v1 and miniF2F-v2c
miniF2F-v1
miniF2F-v2c
Let A, M. and C' be nonnegative integers such that A M+ = 12. What the maxi- mum value of A A-M
Let A, M, and C be nonnegative integers such that À + M +CC 12. What is the maxi- mum value of A.M-C+A.M+MM Prove that one of the following options.
A.C?
(A) 62 (B) 72 (C) 92 (D) 102 (E) 112
Show that it is E.
(A) 62 (B) 72 (C) 92 (D) 102 (E) 112
/-Formal Statement miniF2F-vi-/ theorem amc12_2000_pp (a N) (ho :a+m+ 12)
/-Formal Statement miniF2F-v2-1 theorem amc12_2000_p12 (S: Set N)
a*
(hS: {x 3 aaamen -x=a+
112 := by sorry
m a*cta** + A
a 12))
IsGreatest 62 IsGreatest 72 V
IsGreatest
IsGreatest
102 IsGreatest 112 := by
sorry
35

---

G Effect of introduced changes to ATP performance on Olympiad style questions
To investigate the scale of difficulty, we showcase how the theorem provers perform specifically on IMO, AMC and AIME problems. Figure 3 compared four theorem provers across three miniF2F versions. We note that the strongest provers, Deepseek-Prose Proeece-PPore---7-777 and Goedel-V2-7B. show substantial decline in performance solving twice less IMO problems and 15-50% accuracy decline on AMC. We note that many corrected problems in miniF2F-vvc come from IMO and AMC but not AIME, therefore the performance drop in AIME small across all theorem provers.
miniF2F-v1
miniF2F-v1
miniF2F-v1
2004
34
500
Goederv2
1511
Au0
6
min/F2F-v2c-
Fin/22F-/2 AMC
min/F2F-v2C AIME
18-
16.
1100
10
05V0.5HL
Figure 3: Distribution of solved Olympiad-level (IMO, AMC, AIME) competition problems present 1/2s/2c
in miniF2F-v 1/2ss// across four theorem provers. Theorem prover names were shortened from their original names. Each bar plot also shows the total number of problems present the dataset.
36

---

H Statistics about our modifications
We present the distribution of uncovered errors and inconsistencies in Figure 4 We observe that the majority of the problems in both test and validation sets are simplified and do not reflect the intended difficulty of the problems. Moreover, approximately 40% of formal statements across both sets contained an error, making the evaluation of LLMs on this benchmark less reliable.
miniF2F-test Formal
miniF2F-test Informal
Statements
Statements
Exceaieely Simplified
Simplised
Imckevast
Monniiiiiii Stalements
Unprovable
Woung Sttemant
Usgrovable
Correct
Cornet
16.4% %
18.4%
16.4%
59 %
5.3 %
81.1% %
miniF2F-valid Formal
miniF2F-valid Informal Statements
Statements
Simpltted
Simplited
Wrong/Miesin Staleneat
Ueponsable
Woog Sutement
Ueponobbe
Ourrect
Cucrect
14.8%
17.2%
3.7%
19.7%
%
75.4%
Figure 4: Pie charts of identified formal and informal statement errors within miniF2F benchmark across test and validation sets.
37

---

I Failure topics of tested autoformalization models
To gain deeper insight into the formalization errors the tested autoformalizer models, present our classifications in Tables 9 10 and 11 The categorization of failure cases was performed manually by Lean experts, except for the "Not validated by Lean4 REPL" category, which corresponds to translations that failed compiler verification.
Table 9: Frequency of HERALD autoformalization errors the miniF2F-test dataset.
Failure case classification
Frequency
Wrong/missing/nnoomplee statements or translations
17.5%
Type wrong/mismatch
16.25%
Max/Min of sets/functions wrongly formalized
16.25%
Incomplete set of assumptions
12.5%
Not validated by Lean4 REPL.
7.5%
Digits
7.5%
Finite sets
3.75%
Additional assumpiionshypothesis
3.75%
Common divisors
2.5%
Sequences
2.5%
Others
10.0%
Table 10: Frequency of Kimina-autoffommaiizer autoformalization errors the miniF2F-test dataset.
Failure case classification
Frequency
Wrong/missingnncoopleet statements or translations
57.14%
Not validated by Lean4 REPL.
28.57%
Max/Min of sets/functions wrongly formalized
7.14%
Additional assumpiionshypothesis
7.14%
Table 11: Frequency of o4-mini autoformalization errors the miniF2F-test dataset.
Failure classification
Frequency
Not validated by Lean4 REPL
80.43%
Wrong/missing/nnooplltt statements or translations
6.52%
Max/Min of sets/functions wrongly formalized
6.52%
Incomplete set of assumptions
2.17%
Euclidean spaces
2.17%
Modulus
1.09%
Digits
1.09%
38

---

Toward improving autoformalization models
Improving the performance of autoformalization models requires progress beyond benchmark evalua- tion. A crucial first step is to adopt rigorous and transparent evaluation practices using high-quality. discrepancy- -free benchmarks. This paper takes that step by providing more reliable basis for assessing model accuracy and consistency.
The next important direction is develop high-quality training data that accurately aligns formal and informal mathematical statements. Existing datasets often contain discrepancies or are partially closed-source, which introduce noise during training. Because the miniF2F validation frequently reused for training, more consistent benchmark can have a direct positive effect on model development. Any training example that misaligns formal and informal statements may negatively influence model accuracy and generalization.
is
Beyond data quality, several factors likely to affect model performance, including the distribution of the training corpus (e.g.. mathematical topics and sample diversity), model architecture, reasoning mechanisms, context length, and the use of automated feedback during training. These aspects have been shown to play critical roles in the performance of large language models and general machine learning systems. Incorporating these insights into future autoformalization research help identify effective design choices.
Finally, the field would benefit from systematic ablation studies that isolate the contribution of individual components such as data quality, architecture, and reasoning modules. Reliable benchmarks essential for such analyses, as dataset discrepancies can obscure interpretation. We hope that the availability of correct and comprehensive benchmarks will enable more informative and reproducible studies in this emerging research area.
K Responsibility statement and License information
We plan to release our dataset under the MIT license on GitHub and Hugging Face, The authors of this submission bear the responsibility in case of rights violation.
39


Reviews:
[{"review_id": "adLyK0mf76", "reviewer": "Reviewer_gpAa", "summary": "This paper revisits the miniF2F benchmark for formal theorem proving and autoformalisation in Lean, uncovering widespread issues in miniF2F-v1, including errors and oversimplifications. The authors introduce miniF2F-v2, a corrected version with over 300 human-verified problem pairs. Their evaluation shows that state-of-the-art models perform far worse in end-to-end pipelines than previously reported—dropping from 97% to around 66% accuracy under human judgment. The work highlights the need for stricter evaluation and better alignment between autoformalisation and theorem proving, offering miniF2F-v2 as a more faithful benchmark for future research.", "questions": "- If I understand correctly, all 488 problems have been manually proved in Lean. Given that these formal proofs will now be publicly available online, how do the authors suggest handling or reporting potential data leakage when benchmarking future LLM-based provers that may have seen this data during training?\n\n- Regarding line 179 and Table 3: could you clarify why o4-mini uses a different sampling budget than the other models? Also, which LLM was used to evaluate formalization accuracy in Table 3? Was it o4-mini itself? I’m not entirely clear on why the LLM-verified accuracy is omitted for o4-mini—is it due to concerns about self-evaluation or some other reason? A brief explanation would help.", "limitations": "yes", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 4, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths\n- The original miniF2F benchmark, though impactful, contained numerous errors and ambiguities. In addition, the existence of multiple unofficial versions maintained by different groups has caused confusion within the community. Given the extensive human effort invested in verification, I believe miniF2F-v2 is a significant and much-needed step forward, and I hope it can serve as the definitive version moving forward.\n- The task of generating formal proofs from informal statements is compelling. While it skips the answer-guessing aspect found in benchmarks like PutnamBench, it remains faithful to the spirit of miniF2F.\n\nWeaknesses\n- A key feature of the original miniF2F was its support for multiple formal languages. While it’s understandable that miniF2F-v2 focuses solely on Lean, this limitation should be made clearer in the title (e.g., miniF2F-v2-Lean) and abstract to better manage reader expectations and avoid burying this information in the limitations section.", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your thoughtful and constructive feedback and for your recognition of our contribution.\n\n\n&nbsp;\n\nRegarding the limitation of not including Isabelle and Coq as covered by the original miniF2F, we will add the word Lean to the title of the paper to make this limitation completely clear. Thank you for this suggestion.\n\n&nbsp;\n\n--------\n\n> If I understand correctly, all 488 problems have been manually proved in Lean. Given that these formal proofs will now be publicly available online, how do the authors suggest handling or reporting potential data leakage when benchmarking future LLM-based provers that may have seen this data during training?\n\nYes, your understanding is correct. About data leakage, we can think of two different settings.\n\nSetting 1 is when research papers develop new models or methods (such as training algorithms, etc.) and they want to demonstrate the advantage of their model/method by reporting their accuracy on miniF2F-v2-Lean. In this scenario, we do not have a concrete rule. We think each and every paper can be considered a special case, and the reviewers of each paper will have the best judgement as to what would be scientifically sound. We think after the release of our dataset, if a paper comes forward reporting high accuracy on miniF2F-v2 test without disclosing its training set and releasing a reproducible code, the reviewers of such paper may not be convinced about the technical contribution of the paper. That said, we can imagine a sound paper to openly fine-tune a model directly on the test set of miniF2F in various settings and report the accuracy of resulting models in each setting. We have such studies in the computer vision field that have provided useful insights for the community. Computer vision community has had access to all images of ImageNet and their labels, and through community enforced standards, they have not faced major difficulties in making progress towards better models with better generalization capabilities. \n\nWe also envision a line of research to build upon the work of papers such as LeanDojo, train models from scratch on open source data, and demonstrate better and better ATP accuracies starting from natural language statements of miniF2F-v2 and other benchmarks. We think, gradually, the focus of our community will also expand towards other aspects such as the number of tokens used to achieve a high formal reasoning accuracy, especially in the complete formal reasoning pipeline that we study.\n\nSetting 2 is when models are facing new problems such as proving the problems in IMO 2025 during the Olympiad's timeframe. In this case, we think models can be trained on any data with no need to disclose their sources. This is similar to students being allowed to study any material that they desire during their preparation and with no need to report what they have studied. Each Olympiad has its own rules such as time, no access to internet, etc. An AI model should also follow those rules.\n\n&nbsp;\n\n--------\n\n> Regarding line 179 and Table 3: could you clarify why o4-mini uses a different sampling budget than the other models? Also, which LLM was used to evaluate formalization accuracy in Table 3? Was it o4-mini itself? I’m not entirely clear on why the LLM-verified accuracy is omitted for o4-mini—is it due to concerns about self-evaluation or some other reason? A brief explanation would help.\n\nThis is a great clarification point. In Table 3, DeepSeek-V3 was used for reproducing the pipeline used by Herald Translator, the autoformalization model with highest accuracy published in ICLR 2025. This is the exact pipeline they used and we deployed their own code released with their paper. They had used DeepSeek-V2.5 which is no longer available via API. So, we used Deepseek-V3 and achieved the same result as reported in Herald’s paper. We will clarify this in Table 3 and the text. Specifically, in Tables 2 and 3, we will replace LLM with “Herlad’s automated judge”.\n\nIn our paper, the outputs of Herald and Kimia translator are first evaluated using Herald’s pipeline @1 and @128. The final outputs that come through this pipeline, deemed correct by DeepSeek-V3, are evaluated by human expert. For o4-mini, however, we devised a completely different pipeline which we will make more clear in the paper and the tables.\n\no4-mini is a general purpose model that is not exactly intended to be used for autoformalization in Lean4. Notably, it often writes code in Lean 3, and as far as we know, its autoformalization accuracy on miniF2F is not reported in the literature. However, o4-mini is a strong reasoning model and it can effectively make use of feedback, e.g., feedback from the Lean compiler.\n\nAfter some initial experiments, we concluded that it would not make sense to experiment with o4-mini in the same setting as Herald and Kimina translator because its accuracy will be very low while its computational cost will be much higher than the other two models – worst performance at a higher cost would not be interesting to report for a general purpose model that is not intended for autoformalization. Based on this, we created a new setting for o4-mini in which it gets up to 10 rounds of feedback from the Lean compiler to fix the errors in its Lean statements. This new setting improved the accuracy of o4-mini and reduced its cost which was a better use of our computational budget, yet o4-mini’s final accuracy is far below the accuracy of Kimina translator even pass 1 (it comes close to the accuracy of Herald on miniF2F-v1 and exceeds it on miniF2F-v2). \n\nWe could have dropped our results on o4-mini to only include the results on the two SoTA autoformalization models. But, we think our results on o4-mini is informative and it may be useful to include in the literature. We will explain this more clearly in the paper which has the potential for future research: reasoning models getting feedback from the Lean compiler to improve their output for autoformalization.\n\n\n&nbsp;\n\n--------\n\n\nThank you again for your feedback which improves the clarity of our paper. If you have any additional questions, please let us know."}, {"review_id": "qfG5K3bAys", "reviewer": "Reviewer_ZGEa", "summary": "This paper revises the miniF2F benchmark for evaluating end-to-end mathematical reasoning from natural language to formal proofs. The authors show that prior claims of high component-level accuracy (97% for autoformalization, 69% for theorem proving) do not hold in a full pipeline setting, which achieves only 36% accuracy on the original dataset. They trace this to errors and mismatches in problem formalizations.\n\nThe corrected benchmark, miniF2F-v2, improves pipeline accuracy to 57%, though significant challenges remain. The paper also finds that previous studies tend to overestimate formalization correctness, with true accuracy at 66%, not 97%. This work provides a stronger benchmark that helps faithfully evaluate models formal reasoning capabilities.", "questions": "On line 156: when you check whether “ the first formal output … remains semantically faithful to the source.”, are these verified by human experts or language models? In other places of the paper (like section 4), it is made clear that human experts evaluation is involved, but I can’t seem to find similar statement in this section.", "limitations": "Yes, the authors did mention that the improved benchmark is only for Lean. This is understandable because “patches and fixes” for formal statements are always specific to the target proof engine with their libraries.\n\nThat said, the errors in informal statements identified by the authors can possibly be made generic.", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strength\n\n- The authors inspected in detail the current issues with the MiniF2F benchmark. Errors are well classified into two primary categories and 8 sub-categories. The authors clearly put a significant amount of effort into identifying the errors for over 300 problems by hand. I’m mostly impressed by the corrections in formal statements as some of them would require intensive knowledge about the prover (e.g,, knowing the “right” expressions in Lean to use).\n- The demonstration of flawed existing studies is solid. The authors defined a fair workflow and verified suspiciously high numbers against that. The manual evaluation of the quality by Lean experts made the results more compelling.\n- The improved accuracy when re-evaluating all the models on the improved benchmark (with the fair pipeline) justify the miniF2F-v2 can serve as a clearer and more demanding benchmark.\n\nWeakness\n- My only “complaint” is perhaps on what qualifies a “simplification” of the original problem, as discussed in section 2.2. Not all simplifications are bad — sometimes simplification is even necessary because a problem may not be formalizable at all otherwise due to lack of proper definition/constructions in the existing library.", "was_revised": true, "final_justification": "I am happy with the answers to my questions. I’m keeping my scores.", "rebuttal": "We thank you for your thoughtful and constructive comments and for your recognition of our contribution.\n\n&nbsp;\n\n--------\n\n> My only “complaint” is perhaps on what qualifies a “simplification” of the original problem, as discussed in section 2.2. Not all simplifications are bad — sometimes simplification is even necessary because a problem may not be formalizable at all otherwise due to lack of proper definition/constructions in the existing library.\n\nThis is a great point and hard to define in general. But within the context of miniF2F, simplification has a specific meaning in our paper. The simplifications that we are concerned about are the ones that lead to a discrepancy between the informal and formal statements, i.e., the kind of simplifications that leads to deduction of points in mathematical Olympiads or exams, and we have a specific criteria which is the reasoning steps needed in the formal proof. A simplified problem will require fewer reasoning steps in its proof. **We will clarify this further in the paper and provide more examples in the appendix.**\n\nOne example of simplification is the case where the original IMO1985P6 asks to prove a statement for all real numbers while the miniF2F-v1 version asks to prove that statement only for nonnegative real numbers. Extending the proof of simplified version to negative real numbers is not very difficult but it requires 30 more lines of Lean code.\n\n**We will add a table to report the length of Lean proofs for the simplified problems in miniF2F-v1 vs the the proof lengths for the de-simplified problems in miniF2F-v2. This will demonstrate a significant decrease in the proof lengths for the simplified problems, a proxy for the difficulty of the problems.**\n\nFor the problems in miniF2F, we do not see any case where simplification is necessary due to lack of proper definition/constructions in the existing library, i.e., Mathlib. There are cases where we need new definitions, but such definitions are easy and can usually be done in one line of Lean code. For example, the `Real.rpow` function in Mathlib has a specific definition that deviates from the definition of nth root commonly used in high-school mathematics. This mismatch makes one of the problems in miniF2F unprovable. To address this, we define a new function `Real.qpow` which exactly corresponds to definition of nth root used in high school.\n\n\n&nbsp;\n\n--------\n\n\n> On line 156: when you check whether “ the first formal output … remains semantically faithful to the source.”, are these verified by human experts or language models? In other places of the paper (like section 4), it is made clear that human experts evaluation is involved, but I can’t seem to find similar statement in this section.\n\n\nThe part “remains semantically faithful to the source” is verified by human. You are correct about other sections. We will clarify it in section 3, too.\n\n&nbsp;\n\n--------\n\n\nThank you again for your feedback. The discussions and the table that we will add to the paper based on your feedback improve the clarity of our paper and its contribution. If you have any additional questions, please let us know."}, {"review_id": "9Az2FMUllt", "reviewer": "Reviewer_mdtW", "summary": "This paper revisits the widely used miniF2F benchmark for evaluating formal reasoning systems. The authors identify critical mismatches and errors between the informal and formal statements in the dataset, which negatively impact evaluations of autoformalization and automated theorem proving (ATP) pipelines. To address this, they propose miniF2F-v2, a revised benchmark with over 300 corrected problems. They also conduct a thorough evaluation of state-of-the-art (SoTA) models in end-to-end theorem proving settings, revealing that the original benchmark significantly overestimated model performance due to flawed ground truth. This paper demonstrates that a cleaner and more faithful benchmark can improve both evaluation fidelity and model development.", "questions": "•\tWhat specific types of mathematical statements or constructs most frequently caused failures in autoformalization models?\n\n•\tDo you plan to extend miniF2F-v2 corrections to other formal languages beyond Lean to broaden applicability? For example Coq or Isabelle.\n\n•\tCan you propose modeling or training strategies to reduce the semantic drift observed in current autoformalizers? The results show significant improvement on v2, but performance is still below 60%. What are the key remaining obstacles?\n\n•\tHow might data contamination or overfitting to miniF2F v1 affect the validity of prior autoformalization results?\n\n•\tWould it be possible to provide automated tools or metrics to detect mismatches in future benchmarks?\n\n•\tWould incorporating interactive or verification feedback loops during autoformalization training help close the gap between human and LLM evaluation accuracy?", "limitations": "•\tLimited to the Lean formal system, despite miniF2F’s multi-system nature.\n\n•\tDoes not propose new modeling techniques or training improvements for autoformalization or theorem proving.\n\n•\tBenchmark improvements, while critical, are evaluative rather than methodological contributions.\n\n•\tFocuses on Olympiad-style problems, so generalization to undergraduate-level or research-level formal mathematics is not explored.\n\n•\tHuman verification effort is substantial and may not scale for future expansions.", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 4, "significance": 4, "originality": 2, "strengths_and_weaknesses": "Strengths:\n\n•\tProvides a much-needed clean-up of a widely used benchmark.\n\n•\tIncludes detailed failure analysis and highlights critical flaws in miniF2F-v1.\n\n•\tHighlights the limitations of current LLM-based evaluation methods for autoformalization by contrasting them with expert human verification, demonstrating that LLM self-evaluation greatly overestimates accuracy.\n\n•\tProvides detailed failure mode analysis, categorizing errors into translation failures, autoformalization failures, semantic drift, and success, guiding future methodological improvements.\n\n•\tReleases a valuable and verifiable dataset (miniF2F-v2) with reproducible formal and informal statements.\n\n•\tShows meaningful improvements in end-to-end accuracy using current SoTA models.\n\nWeaknesses:\n\n•\tThe methodological novelty is limited, focusing primarily on dataset correction and benchmark evaluation rather than proposing new autoformalization or theorem proving algorithms.\n\n•\tThe study focuses exclusively on the Lean language despite miniF2F’s availability in other formal systems, potentially limiting its broader impact.\n\n•\tWhile the paper presents extensive empirical evaluations, it lacks in-depth analysis of why current autoformalizers fail at specific mathematical constructs or problem categories beyond general semantic drift.\n\n•\tNo discussion on strategies for improving autoformalization models beyond highlighting benchmark-based discrepancies; readers may expect proposed solutions or training improvements.\n\n•\tThe human evaluation process, though critical to the claims, lacks detail (e.g., annotator agreement or consistency).\n\nQuality:\n\nThe paper is technically sound, with rigorous evaluation methodology, extensive manual verification, and transparent reporting of results and limitations. However, the scope is primarily evaluative rather than methodological.\n\nClarity:\n\nOverall clear, though the dense presentation of empirical results (e.g. Tables 1-7) could be better summarized in prose to guide the reader to key insights. \n\nSignificance:\n\nHighly significant as a benchmark paper, improving data quality for a key dataset in formal reasoning. Its findings on inflated LLM autoformalization evaluations are impactful for the community, though it does not advance modeling techniques itself.\n\nOriginality:\n\nThe originality lies in the benchmark correction and holistic pipeline evaluation, rather than in algorithmic innovation. However, these contributions are critical for realistic progress in automated formal reasoning.", "was_revised": true, "final_justification": "Thanks to the reviewers for engaging. Some minor concerns are still existing and not resolved so I will keep my marginal accept rating.", "rebuttal": "We thank you for your thoughtful and constructive comments and for your recognition of the strengths in our paper. Below, we address your questions and comments.\n\n&nbsp;\n\n--------\n\n\n> The methodological novelty is limited, focusing primarily on dataset correction and benchmark evaluation rather than proposing new autoformalization or theorem proving algorithms.\n\n\nThis is a fair point, but we would like to point out the **NeurIPS CFP for the main track** and the third item on its topics of interest:\n\n- **Evaluation (e.g., methodology, meta studies, replicability and validity, human-in-the-loop)**\n\nWe think we have made a useful contribution for this item in the CFP.\n\n\n&nbsp;\n\n--------\n\n> The study focuses exclusively on the Lean language despite miniF2F’s availability in other formal systems, potentially limiting its broader impact.\nDo you plan to extend miniF2F-v2 corrections to other formal languages beyond Lean to broaden applicability? For example Coq or Isabelle.\n\nWe currently do not have such a plan. Instead we add the word Lean to the title of the paper to make this limitation clear. Our improvements for the natural language statements and proofs in miniF2F-v2-Lean can be useful for users of Isabelle and Coq and also for studies on informal mathematical reasoning. miniF2F-v2 will be a complete benchmark in Lean including human and Lean verified formal/informal statements and formal/informal proofs.\n\n\n&nbsp;\n\n--------\n\n> While the paper presents extensive empirical evaluations, it lacks in-depth analysis of why current autoformalizers fail at specific mathematical constructs or problem categories beyond general semantic drift. \nWhat specific types of mathematical statements or constructs most frequently caused failures in autoformalization models?\n\n\nWe will add additional analysis of failure modes of autoformalization models by categorizing the failures and presenting the accuracies/failures based on the categories. Indeed, there exists some patterns in those failures. For example, Herald consistently makes mistakes in formalizing problems that involve a minimum or maximum bound on a set or a function.\n\n&nbsp;\n\n--------\n\n> No discussion on strategies for improving autoformalization models beyond highlighting benchmark-based discrepancies; readers may expect proposed solutions or training improvements.\n\nThis is a great point. We will add this discussion. We think the first step for improving autoformalization models is to adopt better evaluation practices using high quality benchmarks. This is the step we take in this paper. As the next step, we propose creating high quality training data paired in formal and informal language, and removing any discrepancies from the existing training sets which are often closed source. As the validation set of miniF2F is often used for training, the new benchmark may have a direct positive effect for model development, too. Any training sample that has a discrepancy between its formal and informal statements may have an adverse effect on the accuracy of autoformalization models. We will cite references from the literature on LLMs and general ML. The distribution (math topics, number of samples, etc.) of training set may also have a significant effect on the final accuracy of a model trained on the data. The model architecture, its reasoning modules, context length, automated feedback, etc. have also proved to be influential in the final accuracy of LLMs and other ML models. We will mention this in the paper. Extensive ablation studies are, perhaps, currently lacking in the autoformalization literature. We hope such studies will be added to the literature in the near future. Again, **having correct and complete benchmarks will make such ablation studies more informative because if the benchmarks have discrepancies, interpretation of ablation studies will be noisy and foggy.** We hope our work facilitates future developments in this field.\n\n&nbsp;\n\n--------\n\n> The human evaluation process, though critical to the claims, lacks detail (e.g., annotator agreement or consistency).\n\nWe will provide an appendix detailing the procedures followed by the human annotator.\n\n&nbsp;\n\n--------\n\n> Can you propose modeling or training strategies to reduce the semantic drift observed in current autoformalizers? The results show significant improvement on v2, but performance is still below 60%. What are the key remaining obstacles?\n\nThe remaining obstacles are two fold in our view:\n\nFirst, we need autoformalizers that can translate with higher accuracy. For the start, such autoformalizers need to be trained on higher quality data. Any training sample which has a discrepancy between the informal and formal statements may have a negative effect on the accuracy of an autoformalizer.\n\nThe second fold is about theorem provers. **Our new results which will be added to the paper indicate that, merely on the ATP task, the accuracy of SoTA model, Goedel Prover v2, drops by about 10% when faced with the faithful formal statements that we provide in miniF2F-v2-Lean. This accuracy drops further when Goedel Prover v2 is paired with Kimina translator in the complete formal reasoning pipeline that starts from natural language statements.**\n\nIn this work, we remove the barrier of discrepancies and errors in miniF2F and show that the higher quality benchmark has a positive impact on the accuracy of the complete formal reasoning pipeline that proves theorems starting from natural language statements.\n\n&nbsp;\n\n--------\n\n> How might data contamination or overfitting to miniF2F v1 affect the validity of prior autoformalization results?\n\nThis is an important point. It might be plausible that data contamination and/or overfitting have adversely affected some of the autoformalization and ATP models. However, making such a claim would require an extensive and systematic study of the outputs of these models which is increasingly difficult because the SoTA autoformalization models in the literature, unfortunately, have not released their code and their training data.  When model developers are not open about their training sources – do not release training data and training code – studying their models may not lead to adequate insights and clear conclusions. We hope this practice will change in the near future.\n\nThere may be other ways to study these models, but that would require evaluating them not just on miniF2F, but also on other similar statements that are present and absent from the Internet data, measuring sensitivity of these LLMs to modifications in the problems. Such study would demand a much larger effort by human experts which falls outside the scope of our paper and outside our research interest.\n\n&nbsp;\n\n--------\n\n> Would it be possible to provide automated tools or metrics to detect mismatches in future benchmarks?\n\nWe think this is possible using high quality data and also larger models with advanced reasoning capabilities. For example, one can consider training an advanced LLM with reasoning capabilities on miniF2F-v2 test and validation sets, and then, use that LLM merely as a judge to evaluate the accuracy of autoformalization models that are released in the future. This can also be done for other benchmarks such as Putnam Bench. Having high quality data paired in formal and informal language would be a prerequisite for developing such automated system.\n\n&nbsp;\n\n--------\n\n> Would incorporating interactive or verification feedback loops during autoformalization training help close the gap between human and LLM evaluation accuracy?\n\nYes, this is a great idea for future research, and we believe miniF2F-v2 will be useful for correct evaluation of such study. o4-mini is evidently a general purpose LLM and has not been fine tuned for the task of autoformalization and ATP. Yet, in a previous published paper, using in context learning, we have reported that o4-mini has an impressive capability in incorporating feedback from the Lean compiler. It is likely that using feedback from Lean compiler will also be helpful during fine-tuning with or without RL.\n\n&nbsp;\n\n--------\n\nThank you again for your detailed comments and questions. Addressing the points that you raised improves the clarity of our paper, and the revised paper will provide better insights about possible ways to leverage the miniF2F-v2-Lean for future work. In light of these clarifications and improvements in the paper, we would appreciate it if you consider raising your score. If you have any additional questions, please let us know."}, {"review_id": "zHbdeooYQr", "reviewer": "Reviewer_Vohv", "summary": "The authors evaluate end-to-end formal reasoning pipelines that read mathematical problems in natural language, formalize them in Lean, and generate proofs. They find that state-of-the-art models achieve only 36% accuracy on this complete pipeline, despite individual components reporting much higher accuracies (97% for autoformalization, 69% for theorem proving). Through extensive analysis, they identify significant discrepancies between formal and informal statements in over half of the miniF2F problems. They correct over 300 Lean statements, fix 16 unprovable theorems, and release miniF2F-v2, which improves end-to-end accuracy to 57%.", "questions": "- This is a benchmark study, so why don't you submit to the D&B track? Clearly this paper lacks significant theoretical analysis, it might be more fit to the  D&B track instead of the main track.\n\n- Figure 1 is not necessary as it conveys little information and it occupies a large space in the manuscript. I would suggest to remove it so you can write more content.\n\n- What's the difference between \"Translation failure\" and \"Autoformalization failure\"? In line 49-50, you defined Autoformalization as a kind of translation.\n\n- Can you provide the distribution of systematic errors in the original miniF2F in the main text instead of appendx? Though mentioned, you did not specifiy the location of this distribution in the appendix, which makes reading really inconvenient. \n\n- The sentence spaning line 55-59 is too long, which makes it really difficult to undertand. Please break a long sentence into short sentences, which is a basic requirement for academic paper writing.\n\n- Where does the number 34.8% in line 75 come from?\n\n- I do not understand the last sentence in line 84-85. \"a disconnect between literature and literature?\"\n\n- Line 203, human evaluation also @128? Do you mean human evaluate the problem 128 times?\n\n-Line 209, the data contamination is good point, unfortunetaly you did not dive deeper into it.\n\n- Probably you can merge Table 5-7?\n\n- I do not understand the last sentence in line 236-238. What's the relationship between subset and difficulty?\n\n- Related works could be shorter.", "limitations": "yes", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 2, "strengths_and_weaknesses": "## Strengths\n\n1. The authors found systematical errors in a widely-used benchmark in formal reasoning and categorize errors (unprovable problems, incomplete statements, excessive simplifications, etc.).\n\n2. Unlike previous work relying on LLM evaluation, they conduct expert human verification, revealing that reported autoformalization accuracies are inflated (66% vs. 97% claimed by LLMs).\n\n3. miniF2F-v2 provides a higher-quality benchmark with verified formal proofs and corrected statements that better reflect original problem difficulty.\n\n## Weaknesses\n\n1. Apart from the correction of the miniF2F benchmark, i can hardly tell any other contribution of this work. The work is primarily empirical and doesn't provide significant theoretical insights. It is indeed a significant contribution but I think it is more like a major PR to the originial benchmark instead of a well-draft, ready-to-publish academical article.\n\n2. As I know, the miniF2F benchmark has a v2 version (https://github.com/facebookresearch/miniF2F), whereas you did not mention this at all.\n\n3. Human annotation and verification is also a large systemtic project that needs detailed SOP. Pleasy state how do you recruit the annotaters, how to ensure their expertise, and how to make a SOP so that to minimize the inter-person variance during annotation? This is really important as almost all your contributions come from human effort.\n\n4. The work focuses only on Lean language, though miniF2F exists for other formal verification systems (metamath, HOL Light, Isabelle).  Furthermore, the miniF2F-v2 is still limited to the original 488 problems, which is relatively small for comprehensive evaluation of modern AI systems. More problems will make the your work more valuable.\n\n5. Human verification, while more accurate, doesn't scale well compared to automated evaluation methods.  While the paper identifies problems with LLM evaluation, it doesn't propose robust automated alternatives for evaluating autoformalization quality.\n\n6. The paper doesn't fully address potential data contamination issues in some models, though it notes performance differences that suggest this might be occurring.\n\n7. The paper writing needs improvement. It reads not so good. The authors need to spend more time on writing.", "was_revised": true, "final_justification": "Though the authors did not reply my question about the methodology noverty directly, I will still increase my rating to encourage this kind of contribution to the community.", "rebuttal": "We thank you for your thoughtful and detailed comments and for your recognition of the strengths in our paper. Below, we address your questions and comments.\n\n\n> Apart from the correction of the miniF2F benchmark, i can hardly tell any other contribution of this work ... It is indeed a significant contribution but I think it is more like a major PR to the originial benchmark ...\n> This is a benchmark study, so why don't you submit to the D&B track?\n\nThe NeurIPS CFP for main track lists the topics of interest and the 3rd item on that list is the following:\n\n- **Evaluation (e.g., methodology, meta studies, replicability and validity, human-in-the-loop)**\n\n**We think our paper aligns well with the CFP of the main track.** Although your suggestion of submitting to D&B track is also a sensible possibility, we think the main track is a better fit for our paper given its overall contribution. We have now added experiments on DeepSeek Prover v2 and Goedel Prover v2 extending of our empirical evaluation reporting similar patterns that we believe are insightful for the community.\n\n&nbsp;\n\n---\n\n> As I know, the miniF2F benchmark has a v2 version (https://github.com/facebookresearch/miniF2F), whereas you did not mention this at all.\n\nYes, the version that you cited is the first version of miniF2F that included informal statements. The original version released with the miniF2F paper does not include any informal statements. There are several other versions of miniF2F in the literature that have made improvements, each fixing some of the issues in the formal statements. We will discuss this in the paper and cite that specific version as well.\n\n&nbsp;\n\n---\n\n> Pleasy state how do you recruit the annotaters, how to ensure their expertise, and how to make a SOP so that to minimize the inter-person variance during annotation?\n\nThis is a helpful suggestion. We will provide detailed SOP in a new appendix. Our procedures are similar to the one followed by Putnam Bench. We did not recruit any outside annotators. All the work is done by the authors of the manuscript who have been contributing to open source repositories of Lean language.\n\n&nbsp;\n\n---\n\n> The work focuses only on Lean language, though miniF2F exists for other formal verification systems ... More problems will make the your work more valuable.\n\nWe add \"Lean\" to the title of the paper and the dataset as suggested by reviewer gpAa. Our improvements for the natural language statements and proofs in miniF2F-v2 can be useful for users of Isabelle and Coq and for studies on informal mathematical reasoning. miniF2F-v2 will be a complete benchmark in Lean including human and Lean verified formal/informal statements and formal/informal proofs.\n\nWe think extending the miniF2F beyond the 488 problems can be best done in form of a new benchmark with 488 (or even a few thousands) new problems. If we add, let’s say 50 or 200 new problems to miniF2F-v2, that would cause unnecessary confusions comparing it to v1.\n\n&nbsp;\n\n---\n\n> While the paper identifies problems with LLM evaluation, it doesn't propose robust automated alternatives for evaluating autoformalization quality.\n\nWe will discuss this as an important open research question for the entire community. One of the early papers that considers this question for autoformalization is [37]. We think robust automated alternative evaluation methods may be created for autoformalization of specific mathematical topics in the future. However, it may be the case that we need to first develop models that can perform the task of autoformalization, on a given topic, reliably well, and then, use those same models for robust automated evaluation of other models on those specific topics. It is not clear to us whether one can do robust automated evaluation of autoformalization models prior to having models that can reliably autoformalize a given mathematical topic.\n\nNow that we have fixed all the discrepancies between formal and informal statements in miniF2F, one can consider fine-tuning a capable reasoning LLM (LRM), on our miniF2F-v2 and use it as a judge to automatically evaluate new autoformalization models. There are two important caveats here. One is that typical autoformalization models are small (typically 7B) and they are less capable in reasoning compared to LRMs such as o4 and DeepSeek-v3. This might be a limitation for them to judge the correctness of the outputs of other autoformalization models. An extensive and systematic empirical study may shed light on the capabilities of various models for robust automated evaluation in autoformalization. If they demonstrate such capabilities, they will still need to be fine-tuned on high-quality data so that they can achieve high accuracy on a given benchmark. The accuracy of Kimina translator is around 80% on miniF2F based on our human evaluation, still far from being reliably used as an automated judge. The second caveat is that a single natural language statement may have several correct translations in Lean. So, a mere textual comparison of a formal statement produced by a LLM against a ground truth formal statement may not always lead to correct evaluation of accuracy.\n\nThis point will be a useful discussion added to our paper which suggests how miniF2F-v2 may be leveraged in future developments.\n\n&nbsp;\n\n---\n\n> The paper doesn't fully address potential data contamination issues in some models, though it notes performance differences that suggest this might be occurring.\n\nYou are right – we will discuss this further in the paper. However, we will refrain from making any claims about data contamination of specific models. It might be plausible that data contamination have adversely affected some of the autoformalization models. However, making such a claim would require an extensive and systematic study of the outputs of these models which is increasingly difficult because the SoTA autoformalization models in the literature have not released their training code and their training data. When model developers are not open about their training sources, studying their models may not lead to adequate insights and clear conclusions. We hope this practice will change in the near future.\n\nThere may be other ways to study possible data contamination for these models, but that would require evaluating them not just on miniF2F, but also on other similar statements that are present and absent from the Internet data to measure the sensitivity of these LLMs to modifications in the inputs. Such study on closed-source models would demand a much larger effort by human experts which falls outside the scope of our paper and outside our research interest.\n\n&nbsp;\n\n---\n\n> The paper writing needs improvement. It reads not so good. The authors need to spend more time on writing.\n\nWe will address this feedback and will make sure the final version of the paper reads as smooth as possible.\n\n&nbsp;\n\n--------\n\n> Figure 1 is not necessary as it conveys little information and it occupies a large space in the manuscript.\n\nWe appreciate you being open and sharing your view with us. We will consider your suggestion and make a decision after further deliberation.\n\n&nbsp;\n\n---\n\n> What's the difference between \"Translation failure\" and \"Autoformalization failure\"?\n\nThey are indeed the same. We will unify these terms and use only one of them in the paper.\n\n&nbsp;\n\n----\n\n> Can you provide the distribution of systematic errors in the original miniF2F in the main text instead of appendx?\n\nWe will address this issue per your suggestion.\n\n&nbsp;\n\n---\n\n> The sentence spaning line 55-59 is too long, which makes it really difficult to undertand.\n\nFair point. We will address this and break that sentence.\n\n&nbsp;\n\n---\n\n> Where does the number 34.8% in line 75 come from?\n\nThis number comes from the 4th line in Table 1. Going by the columns from left to right, this number corresponds to the combined accuracy for Herald translator, miniF2F-v2, test, Kimina-ProverDistill-7B.\n\n&nbsp;\n\n---\n\n> I do not understand the last sentence in line 84-85.\n\nThe disconnect that we are referring to in that paragraph is about the mismatches and discrepancies between informal and formal statements in miniF2F-v1. As reported in our paper, a considerable percentage of formal statements are simplified compared to the informal statements. While ATP literature measures the accuracies on the simplified formal statements, the autoformalization literature has built models, such as Kimina Translator, that formalizes the problems without simplification leading to formal statements that are considerably more difficult than the formal statements in miniF2F-v1. As a result, when one evaluates the combines accuracy of a formal reasoning pipeline, the resulting accuracy can be drastically lower than the accuracy of individual modules (ATP and autoformalization). We will clarify this in the final version of the paper.\n\n&nbsp;\n\n---\n\n> Line 203, human evaluation also @128?\n\nNo, our wording in that sentence is too brief which we will revise and clarify. The model is given 1 or 128 attempts to write a proof that passes both the Lean compiler with no error and also the LLM judge – this is the pipeline introduced by Herald at ICLR 2025. The first statement that passes through this system is accepted as the formalization. Once we get the output from Herald's pipeline, we manually evaluate its correctness. In that sentence, we want to compare two cases where the automated pipeline is given 1 vs 128 attempts. Beyond revising the text, we will also replace the term “LLM” with “Herald's automated judge” in Tables 2 and 3.\n\n&nbsp;\n\n---\n\nThank you again for your detailed comments and questions. Your feedback improved the clarity of our contribution and how it can be leveraged for advancing the field. In light of these clarification and improvements, we would appreciate it if you consider raising your score. If you have any other questions, please let us know."}]

Author rebuttal:

Meta-review: The paper studies the popular miniF2F benchmark for formal theorem proving. It compares the typical theorem proving task to the full pipeline involved in participating in a math Olympiad, finding that state-of-the-art models perform much worse in an end-to-end pipeline. The paper finds discrepancies between the informal and formal statements in miniF2F, various other errors in miniF2f, and provides a new miniF2F-v2 with the discrepancies corrected.

The paper had several strengths. miniF2F is widely used in AI theorem proving yet has several flaws. The work found interesting errors in informal statements (e.g., unprovable statements) and formal statements (e.g., simplifying the problem). Their resulting improved version should be impactful for the community. In addition, the task of generating formal proofs from informal statements is compelling and interesting to study further, and the paper provides some nice analysis of performance discrepancies between end-to-end proving and proving given a formal statement. 

On the other hand, the reviewers highlighted some weaknesses. There is a potential for data leakage, since the proofs are provided with the benchmark. While the authors argued that this can be taken care of based on the experimental methodology used, it remains a fair concern for interpreting the results of some methods tested on the benchmark. 

Second, several reviewers noted that the paper only performs analysis on Lean, while the original miniF2F dataset is multi-language. During the discussion the authors acknowledged that they will change the title to make it clear that the paper is about Lean. Given that Lean is one of the main languages considered in AI formal theorem proving, and the paper's contribution was quite substantial in Lean (e.g., providing manually-written proofs), I think this is a sufficient change. 

Finally, two reviewers noted that the paper did not provide a methodological or theoretical innovation. The authors clarified that the NeurIPS CFP has "Evaluation (e.g., methodology, meta studies, replicability and validity, human-in-the-loop)". I agree with this and do not view this as a significant concern for this paper.

Overall, the paper presents an interesting analysis and improved version of the widely-used miniF2F benchmark. This represents an interesting contribution that is likely to be impactful. Reviewers' final ratings were all positive, either suggesting accept or borderline accept. Of the borderline accept cases, substantial concerns were addressed in the rebuttal phase. Taking this and the discussion above into account, I recommend acceptance.
Decision: Accept (poster)