This dataset contains strategic subgoals (lemmas) and their formal proofs for a challenging set of post-2000 International Mathematical Olympiad (IMO) problems. All statements and proofs are formalized in the Lean 4 theorem proving language.
The data was generated using the Decoupled Reasoning and Proving framework, introduced in our paper: Towards Solving More Challenging IMO Problems… See the full description on the dataset page:
https://huggingface.co/datasets/Tencent-IMO/IMO-Lemmas.
