Olympiad-level formal mathematical reasoning with reinforcement learning

Thomas Hubert and Rishi Mehta and Laurent Sartran and Miklós Z Horváth and Goran Žužić and Eric Wieser and Aja Huang and Julian Schrittwieser and Yannick Schroecker and Hussain Masoom and Ottavia Bertolli and Tom Zahavy and Amol Mandhane and Jessica Yung and Iuliya Beloshapka and Borja Ibarz and Vivek Veeriah and Lei Yu and Oliver Nash and Paul Lezeau and Salvatore Mercuri and Calle Sönne and Bhavik Mehta and Alex Davies and Daniel Zheng and Fabian Pedregosa and Yin Li and Ingrid Glehn and Mark Rowland and Samuel Albanie and Ameya Velingker and Simon Schmitt and Edward Lockhart and Edward Hughes and Henryk Michalewski and Nicolas Sonnerat and Demis Hassabis and Pushmeet Kohli and David Silver, Nature, 2025
paper

@article{Hubert2025olympiad,
    author = {Hubert, Thomas and Mehta, Rishi and Sartran, Laurent and Horv{\'a}th, Mikl{\'o}s Z and {\v{Z}}u{\v{z}}i{\'c}, Goran and Wieser, Eric and Huang, Aja and Schrittwieser, Julian and Schroecker, Yannick and Masoom, Hussain and Bertolli, Ottavia and Zahavy, Tom and Mandhane, Amol and Yung, Jessica and Beloshapka, Iuliya and Ibarz, Borja and Veeriah, Vivek and Yu, Lei and Nash, Oliver and Lezeau, Paul and Mercuri, Salvatore and S{\"o}nne, Calle and Mehta, Bhavik and Davies, Alex and Zheng, Daniel and Pedregosa, Fabian and Li, Yin and von Glehn, Ingrid and Rowland, Mark and Albanie, Samuel and Velingker, Ameya and Schmitt, Simon and Lockhart, Edward and Hughes, Edward and Michalewski, Henryk and Sonnerat, Nicolas and Hassabis, Demis and Kohli, Pushmeet and Silver, David},
    title = "Olympiad-level formal mathematical reasoning with reinforcement learning",
    year = "2025",
    month = "November",
    journal = "Nature",
    publisher = "Nature Publishing Group UK London",
    pages = "1--3"
}