Acknowledgment
We would like to thank the International Mathematics Olympiad organization for their support.
AlphaProof’s development was led by Thomas Hubert, Rishi Mehta, and Laurent Sartran. AlphaGeometry 2 and natural language inference efforts were led by Thang Luong.
AlphaProof features key contributions from Hussain Masoom, Aja Huang, Miklós Z. Horváth, Tom Zahavy, Vivek Veeriah, Eric Wieser, Jessica Yung, Lei Yu, Yannick Schroecker, Julian Schrittwieser, Ottavia Bertolli, Borja Ibarz, Edward Lockhart, and Edward Hughes. Developed by. , Mark Rowland, Grace Margand. Alex Davies and Daniel Zheng led the development of informal systems such as final answer determination, with key contributions from Iuliya Beloshapka, Ingrid von Glehn, ying Li, Fabian Pedregosa, Ameya Velingker, and Goran Žužić. Lean expert advice and contributions were provided by Oliver Nash, Bhavik Mehta, Paul Lezeau, Salvatore Mercuri, Lawrence Wu, Calle Soenne, Thomas Murrills, Luigi Massacci, and Andrew Yang. Past contributors include Amol Mandhane, Tom Eccles, Eser Aygün, Zhitao Gong, Richard Evans, Soňa Mokrá, Amin Barekatain, Wendy Shang, Hannah Openshaw, and Felix Gimeno. This work was advised by David Silver and Pushmeet Kohli.
AlphaGeometry 2 development was led by Trieu Trinh and Yuri Chervonyi, with key contributions from Mirek Olšák, Xiaomeng Yang, Hoang Nguyen, Junehyuk Jung, Dawsen Hwang, and Marcelo Menegali. Development of the natural language inference system was led by Golnaz Ghiasi, Garrett Bingham, and YaGuang Li, with key contributions from Swaroop Mishra, Nigamaa Nayakanti, Sidharth Mudgal, Qijun Tan, Junehyuk Jung, Hoang Nguyen, Alex Zhai, Dawsen Hwang, and Mingyang Deng. I did. , Clara Huiyi Fu, Jarrod Khan, Maciej Kula, Cosmodu. Both AlphaGeometry and the natural language inference system were advised by Quoc Le.
David Silver, Quoc Le, Demis Hassabis, and Pushmeet Kohli coordinated and managed the entire project.
We would also like to thank Insuk Seo, Evan Chen, Zigmars Rassevskis, Kari Ragnarsson, Junhwi Bae, Jeonghyun Ahn, Jimin Kim, Hung Pham, Nguyen Nguyen, Son Pham, and Pasin Manurangsi for their help in evaluating the quality of the language inference system. I will. . We would like to thank Jeff Stanway, Jessica Lo, Erica Moreira, Petko Yotov, and Kareem Ayoub for their support with compute provisioning and management. Support and collaboration of Professor Gregor Driner and Dr Geoff Smith (MBE) of the IMO Board of Directors. Tu Vu, Hanjiao Lin, Chiang-Kai Kuan, Vikas Verma, Yifeng Lu, Xingyun Chen, Denny Chou, Vihan Jain, Henryk Michalewski, Xavier Garcia, Arjun Kerr, Rampros Rampur, Kaushal Patel, Kelvin Hsu, Ilya Tolstykhin, Olivier Bousquet, Anton Chiturin, Dustin Zell, CJ Carey, Sam Blackwell. , Abhi Rao, Vahab Milakuni, Benam Neishaboul, Ethan Dyer, Keith Rush, Moritz Farthing, Dan Shved, Ihar Berry, Divyansh Ranjan, Hadi Hashemi, Alexei Bendeberry, Sohail・Hasas Yegane, Shibul Murad, Simon Schmidt, Satinder Baveja, Chris Dyer, Jacob Austin, Wenda Lee, We would like to thank Heng-tze Cheng, Ed Chi, Koray Kavukcuoglu, Oriol Vinyals, Jeff Dean, and Sergey Brin for their support and advice.
Finally, I would like to thank the many contributors to the Lean and Mathlib projects. AlphaProof would not be possible without them.
