AI achieves silver-medal standard solving International Mathematical Olympiad problems

Thanks and appreciation

We thank the International Mathematics Olympiad Organization for its support.

The development of AlphaProof was led by Thomas Hubert, Rishi Mehta and Laurent Sartrand. AlphaGeometry 2 and its natural language reasoning efforts were led by Thang Luong.

AlphaProof was developed with key contributions from Hussein Masoom, Aja Huang, and Miklos Z. Horvath, Tom Zahavi, Vivek Feria, Eric Visser, Jessica Young, Li Yu, Yannick Schroker, Julian Schretweiser, Ottavia Bertoli, Borja Ibarz, Edward Lockhart, Edward Hughes, Mark Rowland, and Grace Margand. Alex Davies and Daniel Zheng led the development of informal systems such as determining the final answer, with major contributions from Yulia Beloshapka, Ingrid von Glenn, Yin Li, Fabian Pedregosa, Amiya Felingker, and Goran Zoetsch. Oliver Nash, Bhavik Mehta, Paul Lizzo, Salvatore Mercury, Lawrence Wu, Callie Swain, Thomas Morels, Luigi Masacci and Andrew Yang advised and contributed as Lean experts. Previous contributors include Amol Mandhan, Tom Eccles, Eser Aygun, Zitao Jung, Richard Evans, Sona Mokra, Amin Barakatin, Wendy Shang, Hannah Openshaw, and Felix Jimeno. This work was advised by David Silver and Pushmeet Kohli.

Trieu Trinh and Yuri Chervonyi led the development of AlphaGeometry 2, with key contributions from Merek Olsak, Xiaoming Yang, Hoang Nguyen, Johnny Hiuc Jung, Dawson Huang, and Marcello Menigalli. The development of the natural language inference system was led by Gulnaz Ghayasi, Garrett Bingham, and Yagong Li, with major contributions from Swaroop Mishra, Nigama Nayakanti, Siddharth Mudgal, Kejun Tan, Johnny Hyuk Jung, Hoang Nguyen, Alex Chai, Dawson Huang, Ming Yang Ding, Clara Hui Hu, Jarrod Kan, Maciej Kula, and Cosmo Du. Both AlphaGeometry and Natural Language Inference Systems were advised by Quoc Le.

David Silver, Kwok Le, Demis Hassabis, and Pushmeet Kohli coordinated and overall managed the project.

We would also like to thank Insuk Seo, Evan Chen, Sigmars Rasscevskis, Kari Ragnarsson, Junhwi Bae, Jeonhyun Ahn, Jimin Kim, Hung Pham, Nguyen Nguyen, Son Pham, and Pasin Manurangsi who helped evaluate the quality of our linguistic reasoning system. Jeff Stanway, Jessica Lu, Erika Moreira, Petko Yotov, and Karim Ayoub for their support in computing provisioning and administration. Professor Gregor Dolinar and Dr Geoff Smith MBE of the IMO Governing Council, for support and collaboration; Tu Fu, Hanzao Lin, Chenkai Kuang, Vikas Verma, Yifeng Lu, Xinyun Chen, Denny Zhu, Vihan Jain, Henrique Michalewski, Rao, Vahab Mirokni, Behnam Nishapur, Ethan Dyer, Keith Rush, Moritz Wiersching, Dan Schved, Ihar Puri, Divyanshu Ranjan, Hadi Hashemi, Alexei Bindipuri, Sohail Hasas Yeganeh, Shibl Murad, Simon Schmidt, Satyinder Bavija, Chris Dyer, Jacob Austin, Wenda Li, Heng Zi Cheng, Ed Qi, Koray. Cavoglu, Oriol Viñales, Jeff Dean and Sergey Brin for their support and advice.

Finally, we would like to thank the many contributors to the Lean and Mathlib projects, without whom AlphaProof would not have been possible.