---
title: "miniF2F-Lean Revisited — paper by Ospanov et al. (2025)"
description: "This NeurIPS 2025 paper examines miniF2F, a widely used benchmark of 488 competition-style math… 53 references, cited by 4 papers here."
authors: ["Azim Ospanov", "Farzan Farnia", "Roozbeh Yousefzadeh"]
year: 2025
venue: "arXiv:2511.03108"
source: "https://arxiv.org/abs/2511.03108"
doi: "10.48550/arxiv.2511.03108"
arxiv: "2511.03108"
licence: "CC BY 4.0 (arXiv)"
licence_url: "http://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/ospanov-2025-minif2f-lean-revisited-reviewing-limitations/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/ospanov-2025-minif2f-lean-revisited-reviewing-limitations/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2025](https://md.research.elamur.ai/free/en/papers/2025/page/14/) / miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward

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

**Authors:** [Azim Ospanov](https://md.research.elamur.ai/free/en/authors/azim-ospanov/), [Farzan Farnia](https://md.research.elamur.ai/free/en/authors/farzan-farnia/) and [Roozbeh Yousefzadeh](https://md.research.elamur.ai/free/en/authors/roozbeh-yousefzadeh/) · **Year:** 2025 · **Venue:** [arXiv:2511.03108](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/) ([NeurIPS 2025](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/2025/)) · **Licence:** [CC BY 4.0 (arXiv)](http://creativecommons.org/licenses/by/4.0/)

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

**Citations:** 0 citations (OpenAlex, 2026-10-14) · 4 in our library, of the 149,439 papers whose bibliographies we read

## Summary
This NeurIPS 2025 paper examines miniF2F, a widely used benchmark of 488 competition-style math problems with paired natural-language and Lean statements. The authors test it as an end-to-end Olympiad pipeline: an AI system must formalize each informal problem in Lean and then prove it, earning credit only when the proof matches the original problem.

Chaining state-of-the-art models (Herald for autoformalization, Kimina Prover for proving) yields only about 35–36% end-to-end accuracy, despite much higher accuracies reported for each component separately. Expert manual review traced much of this gap to mismatches between informal and formal statements in over half of the benchmark, including errors, unprovable theorems and simplified formalizations.

The authors corrected every problem and released miniF2F-v2 in two variants, verified by hand. On v2, the best pipeline reaches roughly 70%. The work shows that benchmark quality and LLM-based grading can distort reported progress in formal reasoning.

## Key points
- **Two variants of miniF2F-v2**, covering both test and validation splits:
  - miniF2F-v2s ("simplified") fixes the informal statements and aligns the formal ones to them exactly.
  - miniF2F-v2c ("competition") restores the original IMO/AMC wording. It keeps multiple-choice options and withholds solutions where the original problem asked for them to be found.
- **Scale of the fixes:** more than 300 Lean 4 statements were corrected, and all 16 originally unprovable theorems were repaired.
- **Autoformalization accuracy is overstated:** Herald reports 97% on miniF2F as judged by an LLM, but expert human checking gives about 66% on v1. Human evaluation covered five autoformalization models.
- **Prover results depend on the fixes:** Kimina Prover scores 70.8% on the original formal statements. Prover accuracy falls on formerly oversimplified problems but rises on previously unprovable ones.
- **Scope and availability:** only the Lean version is covered. The dataset is available at github.com/roozbeh-yz/miniF2F_v2.

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

## Institutions

- [Chinese University of Hong Kong](https://md.research.elamur.ai/free/en/universities/chinese-university-of-hong-kong/) — University, Hong Kong, China · 176 works · 17,536 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

## Cite

Cite as: Azim Ospanov, Farzan Farnia and Roozbeh Yousefzadeh. 2025. miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward. arXiv:2511.03108.

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

```bibtex
@misc{ospanov2025minif2f,
  title = {{miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward}},
  author = {Azim Ospanov, Farzan Farnia and Roozbeh Yousefzadeh},
  year = {2025},
  doi = {10.48550/arxiv.2511.03108},
  eprint = {2511.03108},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2511.03108}
}
```

- [← previous MELABenchv1: Benchmarking Large Language Models against Smaller Fine-Tuned Models for Low-Resource Maltese NLP](https://md.research.elamur.ai/free/en/papers/micallef-2025-melabenchv1-benchmarking-large-language-models/)
- [next → Model Misalignment and Language Change: Traces of AI-Associated Language in Unscripted Spoken English](https://md.research.elamur.ai/free/en/papers/anderson-2025-model-misalignment-language-change-traces/)
- [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/page/14/)

## References

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

1. Alan M Turing. Intelligent machinery, a heretical theory. Philosophia Mathematica, 4(3), 1948. [find](https://scholar.google.com/scholar?q=Alan+M+Turing%2E+Intelligent+machinery%2C+a+heretical+theory%2E+Philosophia+Mathematica%2C+4%283%29%2C+1948%2E)
2. Bruce Pandolfini. Kasparov and Deep Blue: The historic chess match between man and machine. Simon and Schuster, 1997. [find](https://scholar.google.com/scholar?q=Bruce+Pandolfini%2E+Kasparov+and+Deep+Blue%3A+The+historic+chess+match+between+man+and+machine%2E+Simon+and+Schuster%2C+1997%2E)
3. David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al. Mastering the game of Go without human knowledge. Nature, 550(7676):354–359, 2017. [find](https://scholar.google.com/scholar?q=David+Silver%2C+Julian+Schrittwieser%2C+Karen+Simonyan%2C+Ioannis+Antonoglou%2C+Aja+Huang%2C+Arthur+Guez%2C+Thomas+Hubert%2C+Lucas+Baker%2C+Matthew+Lai%2C+Adrian+Bolton%2C+et+al%2E+Mastering+the+game+of+Go+without+human+kn)
4. Stanislas Polu and Ilya Sutskever. [Generative language modeling for automated theorem proving](https://md.research.elamur.ai/free/en/papers/polu-2020-generative-language-modeling-automated-theorem/). arXiv preprint arXiv:2009.03393, 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](https://md.research.elamur.ai/free/en/papers/moura-2021-lean-4-theorem-prover-programming/). Springer-Verlag.
6. Kaiyu Yang and Jia Deng. [Learning to prove theorems via interacting with proof assistants](https://md.research.elamur.ai/free/en/papers/yang-2019-learning-prove-theorems-interacting-proof/). In International Conference on Machine Learning, pages 6984–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 in AI](https://md.research.elamur.ai/free/en/papers/yang-2024-formal-mathematical-reasoning-new-frontier/). In Proceedings of the International Conference on Machine Learning, 2025.
8. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. [miniF2F: A cross-system benchmark for formal Olympiad-level mathematics](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/). In International Conference on Learning Representations, 2021.
9. The AIMO Prize: Airtificial Intelligence Mathematical Olympiad. [https://aimoprize.com/](https://aimoprize.com/). AI achieves silver-medal standard solving international math-[10] Google DeepMind. ematical olympiad problems. https://deepmind.google/discover/blog/ ai-solves-imo-problems-at-silver-medal-level/, 2024. Accessed:… [↗](https://aimoprize.com/)
10. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. [Autoformalization with large language models](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/). Advances in Neural Information Processing Systems, 35, 2022.
11. Haiming Wang, Mert 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, Lo… — [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://md.research.elamur.ai/free/en/papers/wang-2025-kimina-prover-preview-large-formal/)
12. 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](https://md.research.elamur.ai/free/en/papers/liu-2025-atlas-autoformalizing-theorems-through-lifting/), 2025.
13. Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. [Herald: A natural language annotated lean 4 dataset](https://md.research.elamur.ai/free/en/papers/gao-2024-herald-natural-language-annotated-lean/). In The Thirteenth International Conference on Learning Representations, 2025.
14. OpenAI. Introducing openai o3 and o4-mini. introducing-o3-and-o4-mini/, April 2025. [https://openai.com/index/](https://openai.com/index/) [↗](https://openai.com/index/)
15. Lean FRO. A read-eval-print-loop leanprover-community/repl, 2023. 4. for Lean [https://github.com/](https://github.com/) [↗](https://github.com/)
16. 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 m… — [InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning](https://md.research.elamur.ai/free/en/papers/ying-2024-internlm-math-open-math-large/)
17. DeepSeek-AI. Deepseek-v2: A strong, economical, and efficient mixture-of-experts language model, 2024. [find](https://scholar.google.com/scholar?q=DeepSeek%2DAI%2E+Deepseek%2Dv2%3A+A+strong%2C+economical%2C+and+efficient+mixture%2Dof%2Dexperts+language+model%2C+2024%2E)
18. Jiayi Ye, Yanbo Wang, Yue Huang, Dongping Chen, Qihui Zhang, Nuno Moniz, Tian Gao, Werner Geyer, Chao Huang, Pin-Yu Chen, Nitesh V Chawla, and Xiangliang Zhang. [Justice or prejudice? quantifying biases in LLM-as-a-judge](https://md.research.elamur.ai/free/en/papers/ye-2024-justice-prejudice-quantifying-biases-llm/). In The Thirteenth International Conference on Learning Representations, 2025.
19. DeepSeek-AI. Deepseek-v3 technical report, 2024. [find](https://scholar.google.com/scholar?q=DeepSeek%2DAI%2E+Deepseek%2Dv3+technical+report%2C+2024%2E)
20. Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. [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/). arXiv preprint arXiv:2408.08152, 2024.
21. 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](https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-frontier-model-open/). arXiv preprint arXiv:2502.07640, 2025.
22. 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. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcemen… — [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/)
23. 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. [find](https://scholar.google.com/scholar?q=Hanchen+Wang%2C+Tianfan+Fu%2C+Yuanqi+Du%2C+Wenhao+Gao%2C+Kexin+Huang%2C+Ziming+Liu%2C+Payal+Chandak%2C+Shengchao+Liu%2C+Peter+Van+Katwyk%2C+Andreea+Deac%2C+et+al%2E+Scientific+discovery+in+the+age+of+artificial+intelligenc)
24. 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](https://md.research.elamur.ai/free/en/papers/paredes-2023-mathematical-discoveries-program-search-large/). Nature, pages 1–3, 2023.
25. Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. [Solving Olympiad geometry without human demonstrations](https://md.research.elamur.ai/free/en/papers/trinh-2024-solving-olympiad-geometry-without-human/). Nature, 625(7995):476–482, 2024.
26. 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](https://md.research.elamur.ai/free/en/papers/li-2022-competition-level-code-generation-alphacode/). Science, 378(6624):1092–1097, 2022.
27. Can Cui, Wei Wang, Meihui Zhang, Gang Chen, Zhaojing Luo, and Beng Chin Ooi. Alphaevolve: A learning framework to discover novel alphas in quantitative investment. In Proceedings of the 2021 International conference on management of data, pages 2208–2216, 2021. [find](https://scholar.google.com/scholar?q=Can+Cui%2C+Wei+Wang%2C+Meihui+Zhang%2C+Gang+Chen%2C+Zhaojing+Luo%2C+and+Beng+Chin+Ooi%2E+Alphaevolve%3A+A+learning+framework+to+discover+novel+alphas+in+quantitative+investment%2E+In+Proceedings+of+the+2021+Internati)
28. David Silver and Richard S Sutton. Welcome to the era of experience. Google AI, 2025. [find](https://scholar.google.com/scholar?q=David+Silver+and+Richard+S+Sutton%2E+Welcome+to+the+era+of+experience%2E+Google+AI%2C+2025%2E)
29. 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. F. Wu, Fuli Luo, and Chong Ruan. Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-… — [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/)
30. 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: A frontier model for open-source automated theorem proving](https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-frontier-model-open/), 2025.
31. 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](https://md.research.elamur.ai/free/en/papers/zhang-2025-leanabell-prover-posttraining-scaling-formal/), 2025.
32. Kefan Dong and Tengyu Ma. [STP: Self-play LLM theorem provers with iterative conjecturing and proving](https://md.research.elamur.ai/free/en/papers/dong-2025-stp-self-play-llm-theorem/). arXiv preprint arXiv:2502.00212, 2025.
33. Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. Internlm2.5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems, 2024. [find](https://scholar.google.com/scholar?q=Zijian+Wu%2C+Suozhi+Huang%2C+Zhejian+Zhou%2C+Huaiyuan+Ying%2C+Jiayu+Wang%2C+Dahua+Lin%2C+and+Kai+Chen%2E+Internlm2%2E5%2Dstepprover%3A+Advancing+automated+theorem+proving+via+expert+iteration+on+large%2Dscale+lean+problems)
34. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. [Formal mathematics statement curriculum learning](https://md.research.elamur.ai/free/en/papers/polu-2022-formal-mathematics-statement-curriculum-learning/), 2022.
35. 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 llm-based automatic theorem proving](https://md.research.elamur.ai/free/en/papers/xin-2025-bfs-prover-scalable-best-first/), 2025.
36. 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](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/). In Proceedings of the 36th International Conference on Neural Information Processing Systems, pages 26337–2…
37. Haiming Wang et al. [DT-Solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function](https://md.research.elamur.ai/free/en/papers/wang-2023-dt-solver-automated-theorem-proving/). In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 12632–12646, 2023.
38. Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. [HunyuanProver: A scalable data synthesis framework and guided tree search for automated theorem proving](https://md.research.elamur.ai/free/en/papers/li-2024-hunyuanprover-scalable-data-synthesis/), 2025.
39. Roozbeh Yousefzadeh, Xuenan Cao, and Azim Ospanov. [A Lean dataset for International Math Olympiad: Small steps towards writing math proofs for hard problems](https://md.research.elamur.ai/free/en/papers/yousefzadeh-2024-lean-dataset-international-math-olympiad/). Transactions on Machine Learning Research, 2025.
40. Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. [First experiments with neural translation of informal to formal mathematics](https://md.research.elamur.ai/free/en/papers/wang-2018-first-experiments-neural-translation-informal/). In Intelligent Computer Mathematics: 11th International Conference, pages 255–270. Springer, 2018.
41. Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings 13, pages 3–20. Springer, 2020. [find](https://scholar.google.com/scholar?q=Christian+Szegedy%2E+A+promising+path+towards+autoformalization+and+general+artificial+intelligence%2E+In+Intelligent+Computer+Mathematics%3A+13th+International+Conference%2C+CICM+2020%2C+Bertinoro%2C+Italy%2C+July)
42. 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](https://md.research.elamur.ai/free/en/papers/liu-2023-your-code-generated-chatgpt-really/). Advances in Neural Information Processing Systems, 36:21558–21572, 2023.
43. Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, and Junchi Yan. Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval-based approach. In The Thirteenth International Conference on Learning Representations, 2025. [find](https://scholar.google.com/scholar?q=Qi+Liu%2C+Xinhao+Zheng%2C+Xudong+Lu%2C+Qinxiang+Cao%2C+and+Junchi+Yan%2E+Rethinking+and+improving+autoformalization%3A+towards+a+faithful+metric+and+a+dependency+retrieval%2Dbased+approach%2E+In+The+Thirteenth+Intern)
44. Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, and Xiaoxing Ma. [Autoformalize mathematical statements by symbolic equivalence and semantic consistency](https://md.research.elamur.ai/free/en/papers/li-2024-autoformalize-mathematical-statements-symbolic-equivalence/). In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024.
45. Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. [Autoformalizing euclidean geometry](https://md.research.elamur.ai/free/en/papers/murphy-2024-autoformalizing-euclidean-geometry/). In Forty-first International Conference on Machine Learning, 2024.
46. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. [ProofNet: Autoformalizing and formally proving undergraduate-level mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/). arXiv preprint arXiv:2302.12433, 2023.
47. George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnam Bench: Evaluating neural theorem-provers on the Putnam mathematical competition. In The Thirty-eight Conference on Neural Information Processing Systems Datasets an… [find](https://scholar.google.com/scholar?q=George+Tsoukalas%2C+Jasper+Lee%2C+John+Jennings%2C+Jimmy+Xin%2C+Michelle+Ding%2C+Michael+Jennings%2C+Amitayush+Thakur%2C+and+Swarat+Chaudhuri%2E+Putnam+Bench%3A+Evaluating+neural+theorem%2Dprovers+on+the+Putnam+mathemati)
48. 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. Numinamath. [https://github.com/project-numina/aimo-progress-prize/blob/main…](https://github.com/project-numina/aimo-progress-prize/blob/main…) [↗](https://github.com/project-numina/aimo-progress-prize/blob/main…)
49. Jiewen Hu, Thomas Zhu, and Sean Welleck. miniCTX: Neural theorem proving with (long-) contexts. In The Thirteenth International Conference on Learning Representations, 2025. — [miniCTX: Neural Theorem Proving with (Long-)Contexts](https://md.research.elamur.ai/free/en/papers/hu-2024-minictx-neural-theorem-proving-long/)
50. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. [miniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/), 2022.
51. Joshua Vendrow, Edward Vendrow, Sara Beery, and Aleksander Madry. Large language model benchmarks do not test reliability. In NeurIPS Safe Generative AI Workshop 2024, 2024. [find](https://scholar.google.com/scholar?q=Joshua+Vendrow%2C+Edward+Vendrow%2C+Sara+Beery%2C+and+Aleksander+Madry%2E+Large+language+model+benchmarks+do+not+test+reliability%2E+In+NeurIPS+Safe+Generative+AI+Workshop+2024%2C+2024%2E)
52. 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(12):86–92, 2021. [find](https://scholar.google.com/scholar?q=Timnit+Gebru%2C+Jamie+Morgenstern%2C+Briana+Vecchione%2C+Jennifer+Wortman+Vaughan%2C+Hanna+Wallach%2C+Hal+Daum%C3%A9+III%2C+and+Kate+Crawford%2E+Datasheets+for+datasets%2E+Communications+of+the+ACM%2C+64%2812%29%3A86%E2%80%9392%2C+2021%2E)
53. Keiran Paster, Marco Dos Santos, Zhangir Azerbayev, and Jimmy Ba. [OpenWebMath: An open dataset of high-quality mathematical web text](https://md.research.elamur.ai/free/en/papers/paster-2023-openwebmath-open-dataset-high-quality/). In The Twelfth International Conference on Learning Representations, 2023.

*Updated 3 November 2026*