Just caught up with @augpoi who interned at OpenAI with me. It is so cool to see his trajectory in the field of Maths and AI. @augpoi @KunhaoZ Mantas and Marco all interned at OpenAI with me on LLM x Formal Maths. 4 out of 4 stuck with Maths and AI. If there is one achievement I’m proud of of my time at OpenAI, it’s certainly this one. @augpoi worked at Maths Inc is now at DeepMind. @KunhaoZ is now at MetaAI. Mantas and Marco both at Cambridge / Imperial with strong ties to labs as well as @ProjectNumina Strong reminder that at end of the day, the accomplishments are not about the what or the money, it’s all about the people. Yes cheesy. But also true.

Fantastic graph of MiniF2F[0] SotA over the years by the seed prover[1] team (which saturates it!) (h/t @yannfleureau) When we created this benchmark with @KunhaoZ and @jessemhan, getting to 100% seemed completely alien. It took 4 years to get there (though arguably DeepMind probably had capabilities to saturate it last year). It’s at the same time « long » compared to many other benchmarks in the field and extremely short compared to the achievement. These problems are not easy, include IMO problems, and saturating miniF2F happened at the same time the same systems started being competitive in IMOs (as it was intended: as a curriculum from where we were at the time to IMO level). The curve is much less dense in 2021-2023 with mostly work from OpenAI (Reasoning team) and Facebook (@GuillaumeLample et al). Interestingly, I think we (both teams) already had access to the compute needed to achieve much better results; yet, seen from 2025, both our work appear funnily bad (hypertree and curriculum learning). So what was missing? We were already doing a lot of RL but the test-time compute, reasoning RL strategies build up since end of 2024 probably helped a lot the formal modality (techniques re-use, better base models reasoning capabilities). We were also already doing formal/informal mixture to let the model explore in both modalities as well as conjecturing of lemmas to expand test-time compute. I think what we missed the most at the time was simply to push for more scale. (i) More scale in terms of data: informal problem/solution pairs (now aggregated in datasets of 1m+) as well as formal statements. (ii) More scale in terms of test-time compute: lemma generation and proving at a much higher scale today than what was attempted at the time. It's a great lesson in retrospect. I think the only lesson we have to remember which is that with more data and more compute there is no distribution that these models can't learn. One thing I hope these 4 years will bring to the community is a great assistant for Lean 4 that will ease the learning curve and accelerate drastically formalization efforts. The next frontier in the field now is the creation of new maths, which consists in creating new definitions and theories rather than proving exercises. As Buzzard points it, an IMO gold medal is not much more useful than any other new grad student in a maths laboratory and today's models are probably not very useful to accelerate maths research. What will it take to achieve the goal of creating an AI scientist? What is the data to go get to make progress on that front? [0] arxiv.org/abs/2109.00110 [1] arxiv.org/abs/2507.23726