Researchers David Roe and Andrew Sutherland from the Massachusetts Institute of Technology’s Department of Mathematics have been named among the inaugural recipients of the AI for Math grants. These new awards are a collaborative initiative by Renaissance Philanthropy and XTX Markets.
Further distinctions were also awarded to four additional MIT alumni for their individual projects: Anshula Gandhi (’19), Viktor Kunčak (SM ’01, PhD ’07), Gireeja Ranade (’07), and Damiano Testa (PhD ’05).
The inaugural 29 winning projects are poised to bolster mathematical discovery and research through advanced artificial intelligence. These initiatives will provide crucial funding to mathematicians and researchers at universities and various organizations, supporting their efforts to develop AI systems that address several critical tasks in the field.
Researchers Roe and Sutherland, in collaboration with Chris Birkbeck from the University of East Anglia, have been awarded a grant aimed at enhancing automated theorem proving. Their initiative will achieve this by developing crucial connections between the L-Functions and Modular Forms Database (LMFDB) and the Lean4 mathematics library (mathlib).
Automated theorem provers, despite their significant technical complexity, currently suffer from under-resourced development, according to Sutherland. However, the advent of AI technologies, particularly large language models (LLMs), is rapidly diminishing the entry barriers for these sophisticated formal tools. This advancement is poised to make formal verification frameworks readily accessible to working mathematicians.
Mathlib stands as an extensive, community-driven mathematical library tailored for the Lean theorem prover, a sophisticated formal system designed to meticulously verify every step within a proof. This robust library currently houses approximately 100,000 mathematical results, encompassing lemmas, propositions, and theorems. In parallel, the LMFDB operates as a colossal, collaborative online resource, effectively functioning as an encyclopedia for modern number theory. This comprehensive database boasts over a billion concrete statements. Sutherland and Roe serve as the managing editors for the LMFDB.
A new project, funded by a grant awarded to Roe and Sutherland, aims to bridge two key mathematical systems: the L-functions and Modular Forms Database (LMFDB) and mathlib, a comprehensive formalization of mathematics in Lean. This initiative will integrate the LMFDB’s numerical findings into mathlib, presenting them as assertions awaiting formal proof, while simultaneously establishing rigorous formal definitions for the numerical data stored within the LMFDB.
This vital connection is expected to significantly benefit both human mathematicians and artificial intelligence agents. Moreover, it will establish a foundational framework for linking other mathematical databases with formal theorem-proving systems.
Current obstacles to automating mathematical discovery and proof primarily stem from the limited availability of formalized mathematical knowledge, the substantial cost involved in formalizing complex results, and the persistent gap between what is computationally accessible and what is genuinely feasible to formalize.
Researchers, utilizing new funding, are set to develop crucial tools that will link the LMFDB—a vast repository of unformalized mathematical knowledge—with mathlib, a prominent formal proof system. This integration aims to make the extensive database accessible for formal verification. The approach will empower proof assistants to pinpoint specific mathematical elements for formalization, eliminating the need to formalize the entire LMFDB corpus in advance.
Integrating a substantial database of unformalized number-theoretic facts into mathlib would serve as a potent engine for mathematical discovery, according to Roe. He posits that the range of facts a researcher might explore during the pursuit of a theorem or proof far exceeds—exponentially so—the limited set of facts ultimately necessary for formalizing that proof.
Establishing novel mathematical theorems, particularly at the vanguard of knowledge, often demands a reliance on complex computational steps, according to researchers. Andrew Wiles’ landmark proof of Fermat’s Last Theorem serves as a prime example, notably incorporating the “3-5 trick” at a critical stage.
A specific mathematical approach, as noted by Sutherland, relies on the modular curve X_0(15) featuring only a finite set of rational points, none of which correspond to a semi-stable elliptic curve. This principle, known well before Wiles’ contributions, is easily verifiable with modern computer algebra systems, yet it remains impractical to prove with traditional pen-and-paper methods or to formalize simply. Although formal theorem provers are increasingly integrated with computer algebra systems for enhanced verification, utilizing computational outputs from existing mathematical databases offers distinct additional benefits.
Leveraging pre-existing computational results, such as those meticulously stored within the LMFDB, delivers substantial economic advantages by utilizing thousands of CPU-years of prior processing. This approach effectively negates the need for costly and redundant reprocessing. Furthermore, the availability of such precomputed information greatly facilitates the search for specific examples or counterexamples, empowering researchers to conduct extensive explorations without requiring prior knowledge of the search’s potential breadth. Fundamentally, mathematical databases are designed as carefully curated repositories of knowledge, standing distinct from arbitrary collections of facts.
Sutherland noted that number theorists’ emphasis on the conductor within databases of elliptic curves proved pivotal for a significant mathematical breakthrough: the discovery of “murmurations” using machine learning tools.
Roe has outlined the project’s forthcoming initiatives, which include assembling a dedicated team and fostering engagement with both the LMFDB and mathlib communities. The core objectives involve formalizing the fundamental definitions supporting the elliptic curve, number field, and modular form sections of the LMFDB, as well as integrating the capability to conduct LMFDB searches directly from within mathlib.
