Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Roozbeh Yousefzadeh, Xuenan Cao, Azim Ospanov

TL;DR

This work tackles the scarcity of publicly accessible formal proofs for International Math Olympiad problems and the challenge of generating Lean proofs with AI. It provides complete original Lean proofs for remaining miniF2F problems and constructs a lemma-based dataset by decomposing proofs into approachable building blocks to diagnose model capabilities. Evaluations across state-of-the-art provers reveal that short, line-based proofs are easier for existing systems, while longer, plan-driven proofs require more advanced reasoning. Public release of proofs, lemmas, and code supports robust benchmarking and helps steer research toward generalizable formal-proof generation in Lean.

Abstract

Using AI to write formal proofs for mathematical problems is a challenging task that has seen some advancements in recent years. Automated systems such as Lean can verify the correctness of proofs written in formal language, yet writing the proofs in formal language can be challenging for humans and machines. The miniF2F benchmark has 20 IMO problems in its test set, yet formal proofs are available only for 6 of these problems (3 of which are only written by mathematicians). The model with best accuracy can only prove 2 of these 20 IMO problems, from 1950s and 60s, while its training set is a secret. In this work, we write complete, original formal proofs for the remaining IMO problems in Lean along with 3 extra problems from IMO 2022 and 2023. This effort expands the availability of proof currently in the public domain by creating 5,880 lines of Lean proof. The goal of the paper is to pave the way for developing AI models that can automatically write the formal proofs for all the IMO problems in miniF2F and beyond by providing an evaluation benchmark. In this pursuit, we devise a method to decompose the proofs of these problems into their building blocks, constructing a dataset of 1,329 lemmas with more than 40k lines of Lean code. These lemmas are not trivial, yet they are approachable, providing the opportunity to evaluate and diagnose the failures and successes of AI models. We evaluate the ability of the SOTA LLMs on our dataset and analyze their success and failure modes from different perspectives. Our dataset and code is available at: https://github.com/roozbeh-yz/IMO-Steps.

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

TL;DR

This work tackles the scarcity of publicly accessible formal proofs for International Math Olympiad problems and the challenge of generating Lean proofs with AI. It provides complete original Lean proofs for remaining miniF2F problems and constructs a lemma-based dataset by decomposing proofs into approachable building blocks to diagnose model capabilities. Evaluations across state-of-the-art provers reveal that short, line-based proofs are easier for existing systems, while longer, plan-driven proofs require more advanced reasoning. Public release of proofs, lemmas, and code supports robust benchmarking and helps steer research toward generalizable formal-proof generation in Lean.

Abstract

Using AI to write formal proofs for mathematical problems is a challenging task that has seen some advancements in recent years. Automated systems such as Lean can verify the correctness of proofs written in formal language, yet writing the proofs in formal language can be challenging for humans and machines. The miniF2F benchmark has 20 IMO problems in its test set, yet formal proofs are available only for 6 of these problems (3 of which are only written by mathematicians). The model with best accuracy can only prove 2 of these 20 IMO problems, from 1950s and 60s, while its training set is a secret. In this work, we write complete, original formal proofs for the remaining IMO problems in Lean along with 3 extra problems from IMO 2022 and 2023. This effort expands the availability of proof currently in the public domain by creating 5,880 lines of Lean proof. The goal of the paper is to pave the way for developing AI models that can automatically write the formal proofs for all the IMO problems in miniF2F and beyond by providing an evaluation benchmark. In this pursuit, we devise a method to decompose the proofs of these problems into their building blocks, constructing a dataset of 1,329 lemmas with more than 40k lines of Lean code. These lemmas are not trivial, yet they are approachable, providing the opportunity to evaluate and diagnose the failures and successes of AI models. We evaluate the ability of the SOTA LLMs on our dataset and analyze their success and failure modes from different perspectives. Our dataset and code is available at: https://github.com/roozbeh-yz/IMO-Steps.

Paper Structure

This paper contains 26 sections, 1 equation, 3 figures, 10 tables.

Table of Contents

  1. Introduction
  2. IMO: an unknown test set that gets harder every year
  3. Where we are
  4. Our approach
  5. Our contributions
  6. Dataset of approachable lemmas: Stepping stone towards solving challenging IMO problems
  7. Decomposition of the proofs into lemmas
  8. Evaluating the ability of LLMs in proving our lemmas
  9. o3-mini's ability in formal and natural language
  10. Performance of SOTA models on the dataset
  11. Analyzing the proof lengths
  12. Decomposing a proof into its building blocks and extracting new lemmas
  13. Breaking down the structure of a proof
  14. Case of a proof with no intermediate structure
  15. Related work and a discussion on avoiding training/testing set contamination for better evaluation of model generalizations
  16. ...and 11 more sections

Figures (3)

  • Figure 1: Distribution of the length of correct proofs written by LLMs. The histogram also includes the distribution of human-written proof lengths for comparison.
  • Figure F1: Distribution of proof lengths generated by various LLM-based provers on the lemmas dataset (a-e). Histogram (f) illustrates the distribution of length of human-written proofs.
  • Figure G2: Diagrams that illustrate manual redundancy correction in LLM-generated proofs. The overall proof structure remains intact, with only unnecessary elements/structures removed.