Thanks
We thank the International Mathematical Olympiad organization for its support.
AlphaProof was developed by Thomas Hubert, Rishi Mehta and Laurent Sartran. AlphaGeometry 2 and natural language reasoning efforts were conducted by Thang Luong.
AlphaProof was developed with key contributions from Hussain Masoom, Aja Huang, Miklós Z. Horváth, Tom Zahavy, Vivek Veeriah, Eric H. Wieser, Jessica Yung, Lei Yu, Yannick Schroecker, Julian Schrittwieser, Ottavia Bertolli, Borja Lockwardes, Edward Ibarughes , , Mark Rowland, Grace Margand. Alex Davies and Daniel Zheng led the development of informal systems such as determining the final answer, with key contributions from Iuliya Beloshapka, Ingrid von Glehn, Yin Li, Fabian Pedregosa, Ameya Velingker, and Goran Žužić. Oliver Nash, Bhavik Mehta, Paul Lezeau, Salvatore Mercuri, Lawrence Wu, Calle Soenne, Thomas Murrills, Luigi Massacci, and Andrew Yang consulted and contributed as Lean experts. Previous contributors include Amol Mandhane, Tom Eccles, Eser Aygün, Zhitao Gong, Richard Evans, Soňa Mokrá, Amin Barekatain, Wendy Shang, Hannah Openshaw, Felix Gimeno. This work was advised by David Silver and Pushmeet Kohli.
AlphaGeometry 2 was developed by Trieu Trinh and Yuri Chervonyi, with key contributions from Mirek Olšák, Xiaomeng Yang, Hoang Nguyen, Junehyuk Jung, Dawsen Hwang, and Marcelo Menegali. The development of the natural language logic system was done by Golnaz Ghiasi, Garrett Bingham, YaGuang Li, with key contributions from Swaroop Mishra, Nigamaa Nayakanti, Sidharth Mudgal, Qijun Tan, Junehyuk Jung, Hoang Nguyen, Alex Zhai, Dawsen Hwang, Mingyang Deng , Clara Huiyi Hu, Jarrod Kahn, Maciej Kula, Cosmo Du. Both AlphaGeometry and natural language reasoning systems consulted Quoc Le.
David Silver, Quoc Le, Demis Hassabis and Pushmeet Kohli coordinated and managed the overall project.
We would also like to thank Insuk Seo, Evan Chen, Zigmars Rasscevskis, Kari Ragnarsson, Junhwi Bae, Jeonghyun Ahn, Jimin Kim, Hung Pham, Nguyen Nguyen, Son Pham, and Pasin Manurangsi for helping to evaluate the quality of our linguistic inference system. Professor Gregor Dolinar and Dr Geoff Smith MBE from the IMO Board of Directors, for their support and collaboration. and Tu Vu, Hanzhao Lin, Chenkai Kuang, Vikas Verma, Yifeng Lu, Vihan Jain, Henryk Michalewski, Xavier Garcia, Arjun Kar, Lampros Lamprou, Kaushal Patel, Ilya Tolstihen, Olivier Bousquet, Anton Tsitsulin, Dustin Zelle, Blackwell, Abhi Rao , Vahab Mirrokni, Behnam Neyshabur, Ethan Dyer, Keith Rush, Moritz Firsching, Dan Shved, Ihar Bury, Divyanshu Ranjan, Hadi Hashemi, Alexei Bendebury, Soheil Hassas Yeganeh, Shibl Mourad, Simon Schmitt, Chritis Dyer , Jacob Austin, Wenda Li, Heng-tze Cheng, Ed Chi, Koray Kavukcuoglu, Oriol Vinyals, 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 be possible.