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

arXiv: https://arxiv.org/abs/2511.03108 · HTML: https://mlsanity.com/paper/2511.03108/

## Key facts

- Cited by 14 papers in the map (data through 14 Oct 2026).
- Builds on 26 of its 46 references that are in the map.
- First posted on arXiv 5 Nov 2025.

## Builds on (most cited first, 26 of 26)

- [Competition-Level Code Generation with AlphaCode](https://mlsanity.com/paper/2203.07814/) (2022)
- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [Datasheets for Datasets](https://mlsanity.com/paper/1803.09010/) (2018)
- [DeepSeek-V2: A Strong, Economical, and Efficient Mixture-of-Experts Language Model](https://mlsanity.com/paper/2405.04434/) (2024)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Justice or Prejudice? Quantifying Biases in LLM-as-a-Judge](https://mlsanity.com/paper/2410.02736/) (2024)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [OpenWebMath: An Open Dataset of High-Quality Mathematical Web Text](https://mlsanity.com/paper/2310.06786/) (2023)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [miniCTX: Neural Theorem Proving with (Long-)Contexts](https://mlsanity.com/paper/2408.03350/) (2024)
- [AlphaEvolve: A Learning Framework to Discover Novel Alphas in Quantitative Investment](https://mlsanity.com/paper/2103.16196/) (2021)
- [Autoformalizing Euclidean Geometry](https://mlsanity.com/paper/2405.17216/) (2024)
- [A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems](https://mlsanity.com/paper/2411.18872/) (2024)

## Built on by (most cited first, 14 of 14)

- [Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving](https://mlsanity.com/paper/2606.29493/) (2026)
- [TheoremGraph: Bridging Formal and Informal Mathematics](https://mlsanity.com/paper/2606.25363/) (2026)
- [FormalRx: Rectify and eXamine Semantic Failures in Autoformalization](https://mlsanity.com/paper/2607.04655/) (2026)
- [SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization](https://mlsanity.com/paper/2608.29270/) (2026)
- [Fine-Tuning Small Reasoning Models for Quantum Field Theory](https://mlsanity.com/paper/2604.18936/) (2026)
- [Benchmarking Testing in Automated Theorem Proving](https://mlsanity.com/paper/2604.23698/) (2026)
- [Automating Formal Verification with Reinforcement Learning and Recursive Inference](https://mlsanity.com/paper/2605.30914/) (2026)
- [MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis](https://mlsanity.com/paper/2606.13782/) (2026)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [LLM Framework for Discovering Major Mathematical Conjectures: AI's Quest for the Next Riemann Hypothesis](https://mlsanity.com/paper/2607.28632/) (2026)
- [Constructing a Neuro-Symbolic Mathematician from First Principles](https://mlsanity.com/paper/2601.00125/) (2025)
- [Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4](https://mlsanity.com/paper/2605.25556/) (2026)
- [ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization](https://mlsanity.com/paper/2609.34960/) (2026)
- [Sage: Formalization with Semantic Correction](https://mlsanity.com/paper/2609.35790/) (2026)

## Abstract (arXiv)

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.