Databases of Structured Motivated Proofs
The Project
The project aims to significantly enhance AI-driven mathematical research by developing a comprehensive database of motivated proofs, where each idea's origin is clearly documented. By implementing "proof-discovery moves" as Lean tactics, the team will facilitate the formalization and recognition of these proofs, creating a parallel database expressed in Lean. This innovative approach is expected to facilitate the training, evaluation, and interpretation of AI models in mathematics, offering an alternative to traditional theorem-proof pairs that is better suited to the task of actually doing mathematics. The project promises to greatly improve AI performance in mathematical tasks by providing a transparent and structured framework for understanding how mathematicians reason.
The Team
Timothy Gowers is Professor of Combinatorics at the Collège de France, which he combines with a position in the mathematics department at Cambridge and a fellowship at Trinity College. In Cambridge he runs a group in automatic theorem proving, with a focus on understanding the processes that human mathematicians use to find proofs. He received a perfect score in the IMO in 1981 and was awarded a Fields Medal in 1998 for his work in functional analysis and combinatorics. He is the author of Mathematics: A Very Short Introduction and the main editor of The Princeton Companion to Mathematics.
Anand Rao Tadipatri is a second-year PhD student at the University of Cambridge in the human-oriented automatic theorem proving research group of Timothy Gowers. Together with other members of the research group, he has worked on a program to automatically generalize proofs and designing an environment on top of Lean suited towards proof discovery. He is a member of the Lean community and looks forward to the day when interactive theorem provers become mainstream among mathematicians, actively assisting in the proof discovery process.
Anshula Gandhi is a PhD student in Mathematics at the University of Cambridge, specializing in automated theorem proving and the roles of failure and generalization in mathematical research. Her research background also spans knot theory, robotics, and computational astrophysics.
Jacob Loader completed his undergraduate degree at the University of Sydney in mathematics and computer science, followed by a Master's in Mathematics (Part III) at the University of Cambridge. His studies crossed a broad range of fields in pure mathematics, including probability, representation theory and analytic number theory. His current research considers counterexample-guided iteration for existential problems, and implementation of these ideas by metaprogramming in Lean 4.
Jovan Gerbscheid completed the Cambridge mathematical tripos, and he has a gold medal and two bronze medals from the International Mathematical Olympiad. He is now finishing the first year of his PhD in automated theorem proving. He is an active member of the Lean community, specializing in Lean metaprogramming and as of recently he is an official mathlib reviewer.
Jonas Bayer did an undergraduate degree in mathematics at Jacobs University in Bremen. He is currently a PhD student at Cambridge working on automatic theorem proving. He is known for his work with Marco David in successfully formalizing in Isabelle the solution by Davis, Putnam, Robinson and Matiyasevich of Hilbert’s tenth problem.