Elamur Research⌕
☰
home / papers / 2024 / A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems

A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems

Paper · 2024 · Roozbeh Yousefzadeh, Xuenan Cao and Azim Ospanov

Summary

Formal theorem proving in Lean lacks high-quality reference material. Even miniF2F, the community's standard benchmark, has public formal proofs for only 6 of the 20 IMO problems in its test set. Without reference proofs, it is hard to tell where automated provers go wrong. The authors wrote original Lean 4 proofs for the 14 remaining miniF2F IMO problems and for 3 harder problems from IMO 2022 and 2023.

They then split the proofs of 13 of these problems into their component lemmas. The resulting lemmas are easier than full olympiad problems but still non-trivial. They serve as diagnostic stepping stones, much as a teacher assigns simpler sub-problems to locate a student's gaps.

The authors tested Goedel-Prover, DeepSeek-Prover-V1.5-RL and o3-mini on these lemmas. They manually reviewed and categorized o3-mini's informal and formal attempts, including after repeated expert feedback. Current models fail on most lemmas, feedback rarely helps, and the successful proofs tend to be short.

The resource is meant for evaluation, not fine-tuning. Its goal is to separate generalization from retrieval of memorized training data.

Key points

  • New proofs: 17 IMO problems received complete Lean 4 proofs: 14 from the miniF2F test set and 3 from IMO 2022/2023. The paper reports the total as roughly 5.8–5.9k lines (5,790 in one place, 5,880 in another).
  • Lemma dataset: 1,329 lemmas, with over 40k lines of Lean code, were derived from 13 decomposed IMO problems in number theory and algebra. The dataset is released as IMO-Steps on GitHub (roozbeh-yz).
  • Benchmark context: miniF2F's test set contains 244 theorems, 20 of them IMO problems from 1959–2019. LEGO-Prover, the peer-reviewed state of the art, proves only the 1959 problem.
  • Model evaluation: Goedel-Prover, DeepSeek-Prover-V1.5-RL and o3-mini were tested. o3-mini failed on nearly all lemmas, and up to 10 rounds of expert feedback brought little improvement.
  • Evaluation practice: The authors argue for strict separation between training data and the miniF2F test set to avoid contamination. They contrast their approach with AlphaGeometry, LeanDojo and Skill-Mix.

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, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

Cite

Cite as Roozbeh Yousefzadeh, Xuenan Cao and Azim Ospanov. 2024. A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems. arXiv:2411.18872.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2411.18872 · arXiv 2411.18872

@misc{yousefzadeh2024lean,
  title = {{A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems}},
  author = {Roozbeh Yousefzadeh, Xuenan Cao and Azim Ospanov},
  year = {2024},
  doi = {10.48550/arxiv.2411.18872},
  eprint = {2411.18872},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2411.18872}
}

References

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

  1. Sébastien Bubeck, Varun Chandrasekaran, Ronen Eldan, Johannes Gehrke, Eric Horvitz, Ece Kamar, Peter Lee, Yin Tat Lee, Yuanzhi Li, Scott Lundberg, et al. Sparks of artificial general intelligence: Early experiments with GPT-4. arXiv preprint arXiv:2303.12712, 2023.
  2. Kevin Buzzard. Mathematical reasoning and the computer. Bulletin of the American Mathematical Society, 2024. find
  3. Kevin Buzzard and Richard Taylor. A Lean proof of Fermat’s Last Theorem. Technical report, Imperial College of London, 2024. https://imperialcollegelondon.github.io/FLT/blueprint.pdf. ↗
  4. Joseph W Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John Kastner, Anwar Mamat, et al. Cedar: A new language for expressive, fast, safe, and analyzable authorization. Proceedings of the ACM on Programming Languages, 8:670–697,… find
  5. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In 25th International Conference on Automated Deduction, pp. 378–388, 2015. find
  6. Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Li Fei-Fei. ImageNet: A large-scale hierarchical image database. In IEEE Conference on Computer Vision and Pattern recognition, pp. 248–255, 2009. find
  7. Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, et al. The Llama 3 herd of models. arXiv preprint arXiv:2407.21783, 2024.
  8. Emily First, Markus Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 1229–1241, 2023.
  9. 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
  10. Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, 2022.
  11. Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. Large language models are zero-shot reasoners. Advances in Neural Information Processing Systems, 35:22199–22213, 2022.
  12. Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. Advances in Neural Information Processing Systems, 2022.
  13. Hunter Lightman, Vineet Kosaraju, Yuri Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let’s verify step by step. In The Twelfth International Conference on Learning Representations, 2023. — Let's Verify Step by Step
  14. 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.07640, 2025.
  15. OpenAI. OpenAI o3-mini, January 2025. URL https://openai.com/index/openai-o3-mini/. ↗
  16. Bruce Pandolfini. Kasparov and Deep Blue: The historic chess match between man and machine. Simon and Schuster, 1997. find
  17. 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.
  18. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. In The Eleventh International Conference on Learning Representations, 2022.
  19. Benjamin Recht, Rebecca Roelofs, Ludwig Schmidt, and Vaishaal Shankar. Do ImageNet classifiers generalize to ImageNet? In International Conference on Machine Learning, pp. 5389–5400, 2019. find
  20. 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, 625(7995):468–475, 2024.
  21. 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
  22. Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots for theorem proving in Lean. arXiv preprint arXiv:2404.12534, 2024.
  23. Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving Olympiad geometry without human demonstrations. Nature, 625(7995):476–482, 2024.
  24. Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, and Xiaodan Liang. LEGO-Prover: Neural theorem proving with growing libraries. In The Twelfth International Conference on Learning Representations, 2024.
  25. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek-Prover: Advancing theorem proving in LLMs through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024a.
  26. 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. arXiv preprint arXiv:2408.08152, 2024b.
  27. An Yang, Beichen Zhang, Binyuan Hui, Bofei Gao, Bowen Yu, Chengpeng Li, Dayiheng Liu, Jianhong Tu, Jingren Zhou, Junyang Lin, et al. Qwen2.5-math technical report: Toward mathematical expert model via self-improvement. arXiv preprint arXiv:2409.12122, 2024.
  28. Kaiyu Yang, Aidan M Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. In Thirty-seventh Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2023…
  29. Dingli Yu, Simran Kaur, Arushi Gupta, Jonah Brown-Cohen, Anirudh Goyal, and Sanjeev Arora. Skill-Mix: a flexible and expandable family of evaluations for ai models. In The Twelfth International Conference on Learning Representations, 2023. find
  30. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: A cross-system benchmark for formal Olympiad-level mathematics. In International Conference on Learning Representations, 2021.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/yousefzadeh-2024-lean-dataset-international-math-olympiad/