roozbeh-yz/IMO-Steps
IMO-Steps Dataset This dataset is a benchmark that consists of building blocks for 13 IMO problems, and also the complete formal proofs for 20 IMO problems. The topics cover a variety of concepts ranging from divisibility to finite sets and functions. All proof steps are written in Lean 4. All files compile with no error in Lean v4.17.0. The purpose of the dataset is to expose current theorem provers' ability in solving IMO problems and highlight their strengths and weaknesses.… See the full description on the dataset page: https://huggingface.co/datasets/roozbeh-yz/IMO-Steps.
IMO-Steps Dataset
This dataset is a benchmark that consists of building blocks for 13 IMO problems, and also the complete formal proofs for 20 IMO problems. The topics cover a variety of concepts ranging from divisibility to finite sets and functions. All proof steps are written in Lean 4.
All files compile with no error in Lean v4.17.0.
The purpose of the dataset is to expose current theorem provers' ability in solving IMO problems and highlight their strengths and weaknesses.
Paper is available at arxiv.org/abs/2411.18872. It is also published at TMLR: https://openreview.net/forum?id=CrKMqRAhBo.
The dataset is released under MIT license. Contributions are welcome through pull requests.
IMO problems formalized in this paper are as follows:
Performance of SOTA LLMs on the Lemmas Dataset
Distribution of Proof Length of LLM-Generated Proofs
The figure demonstrates that the SOTA LLMs tend to write shorter proofs, which is a potential challenge for lengthier proof procedures that require long-term planning.
Citation
The dataset, motivations and additional results are available here
@article{
yousefzadeh2025a,
title={A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems},
author={Roozbeh Yousefzadeh and Xuenan Cao and Azim Ospanov},
journal={Transactions on Machine Learning Research},
year={2025},
url={https://openreview.net/forum?id=CrKMqRAhBo}
}Versioning
The Lemmas Dataset is explicitly written for the latest available Lean4 version at the moment - v4.17.0. Any subsequent release can impact the released lemmas and some proofs might need future revision.