Solving (some) formal math olympiad problems

OpenAI Blog Papers
formal-mathematics theorem-proving reinforcement-learning curriculum-learning olympiad neural-networks reasoning

Summary

OpenAI achieved a new state-of-the-art 41.2% on the miniF2F formal math olympiad benchmark using a technique called 'statement curriculum learning,' which iteratively trains a neural prover on proofs of increasing difficulty. The approach builds on iterative proof search and retraining over 8 iterations to significantly outperform the previous best of 29.3%.

We built a neural theorem prover for Lean that learned to solve a variety of challenging high-school olympiad problems, including problems from the AMC12 and AIME competitions, as well as two problems adapted from the IMO.
Original Article
View Cached Full Text

Cached at: 04/20/26, 02:55 PM

# Solving (some) formal math olympiad problems Source: [https://openai.com/index/formal-math/](https://openai.com/index/formal-math/) We achieved a new state\-of\-the\-art \(41\.2% vs 29\.3%\) on the[miniF2F⁠\(opens in a new window\)](https://arxiv.org/abs/2109.00110)benchmark, a challenging collection of high\-school olympiad problems\. Our approach, which we call*statement curriculum learning*, consists of manually collecting a set of statements of varying difficulty levels \(without proof\) where the hardest statements are similar to the benchmark we target\. Initially our neural prover is weak and can only prove a few of them\. We iteratively search for new proofs and re\-train our neural network on the newly discovered proofs, and after 8 iterations, our prover ends up being vastly superior when tested on miniF2F\. Formal mathematics is an exciting domain to study because of \(i\) its richness, letting you prove arbitrary theorems which require reasoning, creativity and insight and \(ii\) its similarity to games—where AI has been spectacularly successful—in that it has an automated way of determining whether a proof is successful \(i\.e\., verified by the formal system\)\. As demonstrated in the trivial example below, proving a formal statement requires generating a sequence of proof steps, each proof step consisting in a call to a tactic\.[B](https://openai.com/index/formal-math/#citation-bottom-B) These tactics take mathematical terms as arguments and each tactic call will transform the current statement to prove, into statements that are easier to prove, until nothing is left to prove\.

Similar Articles

@ChrisHayduk: https://x.com/ChrisHayduk/status/2076196217109746095

X AI KOLs Timeline

This article compares two AI approaches for mathematical problem solving: DeepMind's AlphaProof, which uses reinforcement learning in the Lean proof language, and OpenAI's raw LLM that achieved a gold medal at the 2025 International Math Olympiad without formal methods.

Solving math word problems

OpenAI Blog

OpenAI trained a system using verifiers to solve grade school math word problems with 90% of child-level accuracy, nearly doubling fine-tuned GPT-3 performance. The approach addresses language models' weakness in multistep reasoning by training verifiers to evaluate candidate solutions and select the best one.

Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation

arXiv cs.AI

Pythagoras-Prover is a compute-efficient family of Lean theorem provers that achieves strong performance using curriculum supervised fine-tuning and a novel Augmented Lean Formalisation technique. The 4B model surpasses DeepSeek-Prover-V2-671B at pass@32 on MiniF2F-Test, and the 32B model sets a new state-of-the-art among open-source provers.

Our First Proof submissions

OpenAI Blog

OpenAI submitted proof attempts for the First Proof challenge, a research-level math competition testing whether AI can produce correct, checkable proofs. The company's internal model successfully solved at least five of the ten problems, demonstrating significant progress in sustained reasoning and rigorous mathematical thinking.