---
title: "MiniF2F: a cross-system benchmark for formal — Zheng 2021"
description: "Neural theorem proving research has mostly been evaluated on library-specific test splits, such as those in HOList, CoqGym or LeanStep."
authors: ["Kunhao Zheng", "Jesse Michael Han", "Stanislas Polu"]
year: 2021
venue: "arXiv:2109.00110"
source: "https://arxiv.org/abs/2109.00110"
doi: "10.48550/arxiv.2109.00110"
arxiv: "2109.00110"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2021](https://md.research.elamur.ai/free/en/papers/2021/page/3/) / MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics

# MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics

**Authors:** [Kunhao Zheng](https://md.research.elamur.ai/free/en/authors/kunhao-zheng/), [Jesse Michael Han](https://md.research.elamur.ai/free/en/authors/jesse-michael-han/), [Stanislas Polu](https://md.research.elamur.ai/free/en/authors/stanislas-polu/) · **Year:** 2021 · **Venue:** arXiv:2109.00110 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/2109.00110) · [PDF](https://arxiv.org/pdf/2109.00110v2) · [DOI 10.48550/arxiv.2109.00110](https://doi.org/10.48550/arxiv.2109.00110) · [arXiv 2109.00110](https://arxiv.org/abs/2109.00110) · [OpenAlex](https://openalex.org/W3197040007)

**Citations:** 26 citations (openalex-snapshot · 2026-10-14) · [228](#cited-by) in our library, of the 140673 papers whose bibliographies we read

## Summary
Neural theorem proving research has mostly been evaluated on library-specific test splits, such as those in HOList, CoqGym or LeanStep. Results from different proof assistants therefore cannot be compared directly. miniF2F addresses this with a shared benchmark of 488 competition-style statements, each formalized by hand. The problems come from AMC, AIME and IMO, from the MATH dataset, and from high-school and undergraduate coursework. The same problems are encoded in Metamath and Lean, with Isabelle and HOL Light partly covered. The statements are split into equal, stratified validation and test sets. The work is motivated by the IMO Grand Challenge, which asks for machine-checkable proofs of formally stated problems. As baselines, the authors evaluate GPT-f on Metamath, GPT-f/PACT on Lean, and Lean's built-in `tidy` tactic search. Lean GPT-f is the strongest of the three: it proves every statement that either other baseline solves. Problems that need more than about two non-trivial reasoning steps, or a hard-to-guess witness, generally stay unsolved. The benchmark is a common yardstick for the field and is intended to grow through community contributions.

## Key points
- miniF2F v1 has 244 test and 244 validation statements. The algebra, number theory and inequality problems come from IMO, AIME, AMC, five difficulty levels of MATH, and custom exercises. Geometry and combinatorics are mostly excluded because current formal libraries make them hard to formalize.
- Formats and licenses: Metamath is released under MIT, and Lean and Isabelle under Apache. Releases are frozen versions on GitHub (openai/miniF2F), and a Coq port is invited.
- Formalizing one statement took trained practitioners about 15 minutes, and reviewing it took about half that.
- Answer-dependent problems are adapted in three ways:
  - Multiple-choice questions keep only the correct option.
  - Word problems are modeled explicitly, or dropped if formalizing them would be most of the difficulty.
  - "Find all…" problems include the answer in the statement, which can make them easier.
- Baselines compared were Metamath GPT-f, Lean `tidy` and Lean GPT-f/PACT. On statements taken from MATH, Lean GPT-f solved the most at every difficulty level, while Metamath GPT-f solved almost none.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

Fields: [Mathematics & statistics](https://md.research.elamur.ai/free/en/shelves/mathematics/)

## Cited by

Cited by

228 papers of our library cite it (of the 140673 whose bibliographies we read); 17 of them have a page here, 211 not yet.

- [Large Language Models for Mathematical Reasoning: Progresses and Challenges](https://md.research.elamur.ai/free/en/papers/ahn-2024-large-language-models-mathematical-reasoning/)
- [Llemma: An Open Language Model For Mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-llemma-open-language-model-mathematics/)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/)
- [Large Language Monkeys: Scaling Inference Compute with Repeated Sampling](https://md.research.elamur.ai/free/en/papers/brown-2024-large-language-monkeys-scaling-inference/)
- [Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models](https://md.research.elamur.ai/free/en/papers/gao-2024-omni-math-universal-olympiad-level/)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/)
- [HyperTree Proof Search for Neural Theorem Proving](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/)
- [GSM-Plus: A Comprehensive Benchmark for Evaluating the Robustness of LLMs as Mathematical Problem Solvers](https://md.research.elamur.ai/free/en/papers/li-2024-gsm-plus-comprehensive-benchmark-evaluating/)
- [LILA: A Unified Benchmark for Mathematical Reasoning](https://md.research.elamur.ai/free/en/papers/mishra-2022-lila-unified-benchmark-mathematical-reasoning/)
- [Formal Mathematics Statement Curriculum Learning](https://md.research.elamur.ai/free/en/papers/polu-2022-formal-mathematics-statement-curriculum-learning/)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://md.research.elamur.ai/free/en/papers/ren-2025-deepseek-prover-v2-advancing-formal/)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://md.research.elamur.ai/free/en/papers/shao-2024-deepseekmath-pushing-limits-mathematical-reasoning/)
- [Autoformalization with Large Language Models](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-advancing-theorem-proving/)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-v1-5-harnessing/)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://md.research.elamur.ai/free/en/papers/yang-2023-leandojo-theorem-proving-retrieval-augmented/)
- [A Survey of Large Language Models](https://md.research.elamur.ai/free/en/papers/zhao-2023-survey-large-language-models/)

## Cite

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{zheng2021minif2f,
  title = {{MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics}},
  author = {Zheng, Kunhao and Han, Jesse Michael and Polu, Stanislas},
  year = {2021},
  doi = {10.48550/arxiv.2109.00110},
  eprint = {2109.00110},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2109.00110}
}
```

- [← previous Mind the Style of Text! Adversarial and Backdoor Attacks Based on Text Style Transfer](https://md.research.elamur.ai/free/en/papers/qi-2021-mind-style-text-adversarial-backdoor/)
- [next → Minor changes make a difference: a case study on the consistency of UD-based dependency parsers](https://md.research.elamur.ai/free/en/papers/kalpakchi-2021-minor-changes-make-difference-case/)
- [↑ back to papers of 2021](https://md.research.elamur.ai/free/en/papers/2021/page/3/)

## References

29 references, 6 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher order logic theorem proving. In International Conference on Machine Learning, pp. 454–463. PMLR, 2019a. [find](https://scholar.google.com/scholar?q=Kshitij+Bansal%2C+Sarah+Loos%2C+Markus+Rabe%2C+Christian+Szegedy%2C+and+Stewart+Wilcox%2E+Holist%3A+An+environment+for+machine+learning+of+higher+order+logic+theorem+proving%2E+In+International+Conference+on+Machin)
2. Kshitij Bansal, Christian Szegedy, Markus N Rabe, Sarah M Loos, and Viktor Toman. Learning to reason in large theories without imitation. arXiv preprint arXiv:1905.10501, 2019b. [find](https://scholar.google.com/scholar?q=Kshitij+Bansal%2C+Christian+Szegedy%2C+Markus+N+Rabe%2C+Sarah+M+Loos%2C+and+Viktor+Toman%2E+Learning+to+reason+in+large+theories+without+imitation%2E+arXiv+preprint+arXiv%3A1905%2E10501%2C+2019b%2E)
3. Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel Ziegler, Jeffrey Wu, Clemens Winter, Chri… [find](https://scholar.google.com/scholar?q=Tom+Brown%2C+Benjamin+Mann%2C+Nick+Ryder%2C+Melanie+Subbiah%2C+Jared+D+Kaplan%2C+Prafulla+Dhariwal%2C+Arvind+Neelakantan%2C+Pranav+Shyam%2C+Girish+Sastry%2C+Amanda+Askell%2C+Sandhini+Agarwal%2C+Ariel+Herbert%2DVoss%2C+Gretchen)
4. Curran Associates, Inc., 2020. URL [https://proceedings.neurips.cc/paper/2020/file/1457c0d6bfcb4967418bfb8ac142f64a-Paper.pdf](https://proceedings.neurips.cc/paper/2020/file/1457c0d6bfcb4967418bfb8ac142f64a-Paper.pdf). [↗](https://proceedings.neurips.cc/paper/2020/file/1457c0d6bfcb4967418bfb8ac142f64a-Paper.pdf)
5. Kevin Buzzard, Johan Commelin, and Patrick Massot. Lean perfectoid spaces. [https://leanprover-community.github.io/lean-perfectoid-spaces/](https://leanprover-community.github.io/lean-perfectoid-spaces/), 2019. [↗](https://leanprover-community.github.io/lean-perfectoid-spaces/)
6. Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Li Fei-Fei. Imagenet: A large-scale hierarchical image database. In 2009 IEEE conference on computer vision and pattern recognition, pp. 248–255. [find](https://scholar.google.com/scholar?q=Jia+Deng%2C+Wei+Dong%2C+Richard+Socher%2C+Li%2DJia+Li%2C+Kai+Li%2C+and+Li+Fei%2DFei%2E+Imagenet%3A+A+large%2Dscale+hierarchical+image+database%2E+In+2009+IEEE+conference+on+computer+vision+and+pattern+recognition%2C+pp%2E+248%E2%80%93)
7. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. arXiv preprint arXiv:2102.06203, 2021. [find](https://scholar.google.com/scholar?q=Jesse+Michael+Han%2C+Jason+Rute%2C+Yuhuai+Wu%2C+Edward+W+Ayers%2C+and+Stanislas+Polu%2E+Proof+artifact+co%2Dtraining+for+theorem+proving+with+language+models%2E+arXiv+preprint+arXiv%3A2102%2E06203%2C+2021%2E)
8. Maximilian P. L. Haslbeck, Tobias Nipkow, and Simon Wimmer. //www21.in.tum.de/˜wimmers/proofground/, 2019. [find](https://scholar.google.com/scholar?q=Maximilian+P%2E+L%2E+Haslbeck%2C+Tobias+Nipkow%2C+and+Simon+Wimmer%2E+%2F%2Fwww21%2Ein%2Etum%2Ede%2F%CB%9Cwimmers%2Fproofground%2F%2C+2019%2E)
9. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. arXiv preprint arXiv:2103.03874, 2021. [find](https://scholar.google.com/scholar?q=Dan+Hendrycks%2C+Collin+Burns%2C+Saurav+Kadavath%2C+Akul+Arora%2C+Steven+Basart%2C+Eric+Tang%2C+Dawn+Song%2C+and+Jacob+Steinhardt%2E+Measuring+mathematical+problem+solving+with+the+math+dataset%2E+arXiv+preprint+arXiv%3A) [our card](https://md.research.elamur.ai/free/en/papers/hendrycks-2021-measuring-mathematical-problem-solving-math/)
10. The mathlib Community. The lean mathematical library. In Jasmin Blanchette and Catalin Hritcu (eds.), Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pp. 367–381. [find](https://scholar.google.com/scholar?q=The+mathlib+Community%2E+The+lean+mathematical+library%2E+In+Jasmin+Blanchette+and+Catalin+Hritcu+%28eds%2E%29%2C+Proceedings+of+the+9th+ACM+SIGPLAN+International+Conference+on+Certified+Programs+and+Proofs%2C+CPP+)
11. ACM, 2020. doi: 10.1145/3372885.3373824. URL https://doi.org/10.1145/3372885.3373824. [↗](https://doi.org/10.1145/3372885.3373824)
12. Proof ground. https: Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 34, pp. 2967–2974, 2020. [find](https://scholar.google.com/scholar?q=Proof+ground%2E+https%3A+Aditya+Paliwal%2C+Sarah+Loos%2C+Markus+Rabe%2C+Kshitij+Bansal%2C+and+Christian+Szegedy%2E+Graph+representations+for+higher%2Dorder+logic+and+theorem+proving%2E+In+Proceedings+of+the+AAAI+Confer)
13. Denis Paperno, Germán Kruszewski, Angeliki Lazaridou, Quan Ngoc Pham, Raffaella Bernardi, Sandro Pezzelle, Marco Baroni, Gemma Boleda, and Raquel Fernández. The LAMBADA dataset: Word prediction requiring a broad discourse context. In Proceedings of the 54th Annual Meeting of the Association for Co… [find](https://scholar.google.com/scholar?q=Denis+Paperno%2C+Germa%CC%81n+Kruszewski%2C+Angeliki+Lazaridou%2C+Quan+Ngoc+Pham%2C+Raffaella+Bernardi%2C+Sandro+Pezzelle%2C+Marco+Baroni%2C+Gemma+Boleda%2C+and+Raquel+Ferna%CC%81ndez%2E+The+LAMBADA+dataset%3A+Word+prediction+requ) [our card](https://md.research.elamur.ai/free/en/papers/paperno-2016-lambada-dataset-word-prediction-requiring/)
14. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020. [find](https://scholar.google.com/scholar?q=Stanislas+Polu+and+Ilya+Sutskever%2E+Generative+language+modeling+for+automated+theorem+proving%2E+arXiv+preprint+arXiv%3A2009%2E03393%2C+2020%2E) [our card](https://md.research.elamur.ai/free/en/papers/polu-2020-generative-language-modeling-automated-theorem/)
15. Pranav Rajpurkar, Jian Zhang, Konstantin Lopyrev, and Percy Liang. Squad: 100, 000+ questions for machine comprehension of text. In Jian Su, Xavier Carreras, and Kevin Duh (eds.), Proceedings of the 2016 Conference on Empirical Methods in Natural Language Processing, EMNLP 2016, Austin, Texas, USA,… [find](https://scholar.google.com/scholar?q=Pranav+Rajpurkar%2C+Jian+Zhang%2C+Konstantin+Lopyrev%2C+and+Percy+Liang%2E+Squad%3A+100%2C+000%2B+questions+for+machine+comprehension+of+text%2E+In+Jian+Su%2C+Xavier+Carreras%2C+and+Kevin+Duh+%28eds%2E%29%2C+Proceedings+of+the+2) [our card](https://md.research.elamur.ai/free/en/papers/rajpurkar-2016-squad-100-000-questions-machine/)
16. David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. Analysing mathematical reasoning abilities of neural models. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. [find](https://scholar.google.com/scholar?q=David+Saxton%2C+Edward+Grefenstette%2C+Felix+Hill%2C+and+Pushmeet+Kohli%2E+Analysing+mathematical+reasoning+abilities+of+neural+models%2E+In+7th+International+Conference+on+Learning+Representations%2C+ICLR+2019%2C+) [our card](https://md.research.elamur.ai/free/en/papers/saxton-2019-analysing-mathematical-reasoning-abilities-neural/)
17. OpenReview.net, 2019. URL [https://openreview.net/forum?id=H1gR5iR5FX](https://openreview.net/forum?id=H1gR5iR5FX). [↗](https://openreview.net/forum?id=H1gR5iR5FX)
18. Peter Scholze. Liquid tensor experiment. [https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/](https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/), 2020. [↗](https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/)
19. Daniel Selsam, Kevin Buzzard, Reid Barton, Percey Liang, Sarah Loss, and Freek Wiedijk. Imo grand challenge. [https://imo-grand-challenge.github.io/](https://imo-grand-challenge.github.io/), 2019. [↗](https://imo-grand-challenge.github.io/)
20. G. Sutcliffe. The CADE ATP System Competition - CASC. AI Magazine, 37(2):99–101, 2016. [find](https://scholar.google.com/scholar?q=G%2E+Sutcliffe%2E+The+CADE+ATP+System+Competition+%2D+CASC%2E+AI+Magazine%2C+37%282%29%3A99%E2%80%93101%2C+2016%2E)
21. G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning, 59(4):483–502, 2017. [find](https://scholar.google.com/scholar?q=G%2E+Sutcliffe%2E+The+TPTP+Problem+Library+and+Associated+Infrastructure%2E+From+CNF+to+TH0%2C+TPTP+v6%2E4%2E0%2E+Journal+of+Automated+Reasoning%2C+59%284%29%3A483%E2%80%93502%2C+2017%2E)
22. Alex Wang, Amanpreet Singh, Julian Michael, Felix Hill, Omer Levy, and Samuel R. Bowman. GLUE: A multi-task benchmark and analysis platform for natural language understanding. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. [find](https://scholar.google.com/scholar?q=Alex+Wang%2C+Amanpreet+Singh%2C+Julian+Michael%2C+Felix+Hill%2C+Omer+Levy%2C+and+Samuel+R%2E+Bowman%2E+GLUE%3A+A+multi%2Dtask+benchmark+and+analysis+platform+for+natural+language+understanding%2E+In+7th+International+Con) [our card](https://md.research.elamur.ai/free/en/papers/wang-2018-glue-multi-task-benchmark-analysis/)
23. OpenReview.net, 2019. URL [https://openreview.net/forum?id=rJ4km2R5t7](https://openreview.net/forum?id=rJ4km2R5t7). [↗](https://openreview.net/forum?id=rJ4km2R5t7)
24. Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. Naturalproofs: Mathematical theorem proving in natural language. arXiv preprint arXiv:2104.01112, 2021. [find](https://scholar.google.com/scholar?q=Sean+Welleck%2C+Jiacheng+Liu%2C+Ronan+Le+Bras%2C+Hannaneh+Hajishirzi%2C+Yejin+Choi%2C+and+Kyunghyun+Cho%2E+Naturalproofs%3A+Mathematical+theorem+proving+in+natural+language%2E+arXiv+preprint+arXiv%3A2104%2E01112%2C+2021%2E)
25. Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. CoRR, abs/1608.02644, 2016. URL http://arxiv.org/abs/1608.02644. [↗](http://arxiv.org/abs/1608.02644)
26. Freek Wiedijk. Formalizing 100 theorems. [https://www.cs.ru.nl/˜freek/100/](https://www.cs.ru.nl/˜freek/100/), 2008. [↗](https://www.cs.ru.nl/˜freek/100/)
27. Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger Baker Grosse. INT: an inequality benchmark for evaluating generalization in theorem proving. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. [find](https://scholar.google.com/scholar?q=Yuhuai+Wu%2C+Albert+Jiang%2C+Jimmy+Ba%2C+and+Roger+Baker+Grosse%2E+INT%3A+an+inequality+benchmark+for+evaluating+generalization+in+theorem+proving%2E+In+9th+International+Conference+on+Learning+Representations%2C+I)
28. OpenReview.net, 2021. URL [https://openreview.net/forum?id=O6LPudowNQm](https://openreview.net/forum?id=O6LPudowNQm). [↗](https://openreview.net/forum?id=O6LPudowNQm)
29. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning, pp. 6984–6994. PMLR, 2019. [find](https://scholar.google.com/scholar?q=Kaiyu+Yang+and+Jia+Deng%2E+Learning+to+prove+theorems+via+interacting+with+proof+assistants%2E+In+International+Conference+on+Machine+Learning%2C+pp%2E+6984%E2%80%936994%2E+PMLR%2C+2019%2E)