Scalable Theorem Proving via Mathematical Databases
The Project
This project seeks to increase the scale of mathematical content accessible to automated theorem provers by creating an interface between the Lean mathematical library (mathlib) and the L-functions and Modular Forms Database (LMFDB). By connecting mathlib's collection of approximately 100,000 mathematical results with the LMFDB's repository of over a billion concrete statements, we aim to expand the capabilities of both human mathematicians and AI agents. The project will develop new Lean tactics and establish a framework for integrating other mathematical databases with formal theorem proving systems, paving the way for scalable mathematical discovery.
The Team
Christopher Birkbeck is a Lecturer in pure mathematics at the University of East Anglia, specialising in number theory. His research has involved studying and computing p-adic modular forms, and his current work is in mathematical formalisation, focusing on the theory of modular forms in Lean. Birkbeck completed his PhD at the University of Warwick under the supervision of Lassina Dembele and John Cremona, and subsequently held a postdoctoral fellowship at UCL.
David Roe is a Principal Research Scientist in the Department of Mathematics at MIT, where he studies computational number theory and arithmetic geometry with a particular focus on p-adic numbers (an analogue of the real numbers with a different notion of distance designed to measure divisibility by a fixed prime number). The p-adic numbers played a central role in his journey toward building computational tools for the mathematical community, which began with his work on p-adic computation in SageMath. He serves as a Managing Editor for the L-functions and Modular Forms Database (LMFDB), a collection of mathematical objects arising in number theory and arithmetic geometry; he is also one of the founders of researchseminars.org, a site created during the pandemic to connect mathematicians to online research seminars.
Andrew Sutherland is the Senior Research Scientist of Mathematics at MIT, with a research program focused on computational aspects of arithmetic geometry and number theory. He has played a major role in several large scale research collaborations, including the Polymath project on Bounded Gaps Between Primes, the L-functions and Modular Forms Database, and the Simons Collaboration on Arithmetic Geometry, Number Theory, and Computation. Sutherland currently serves as an Editor of Mathematics of Computation, Editor in Chief of Research in Number Theory, Managing Editor of the L-Functions and Modular Forms Database, Scientific Advisor Board member of the Institute for Computational and Experimental Research in Mathematics, President of the Number Theory Foundation, and Fellow of the American Mathematical Society.