MIT Department of Mathematics researchers David Roe ’06 and Andrew Sutherland ’90, PhD ’07, are among the inaugural recipients of the AI for Math grants launched by Renaissance Philanthropy and XTX Markets. The initiative supports groundbreaking research at the intersection of artificial intelligence and mathematical discovery, with 29 projects selected nationwide to advance the use of AI in mathematics. Four additional MIT alumni were also honored: Anshula Gandhi ’19, Viktor Kunčak SM ’01, PhD ’07, Gireeja Ranade ’07, and Damiano Testa PhD ’05, each recognized for distinct projects aimed at harnessing AI to push the boundaries of mathematical research. Roe and Sutherland, along with Chris Birkbeck of the University of East Anglia, will use their grant to strengthen automated theorem proving by connecting two major mathematical resources: the L-Functions and Modular Forms Database (LMFDB) and the Lean4 mathematics library, known as mathlib. The LMFDB is a comprehensive, collaborative online encyclopedia of modern number theory, housing over 109 concrete mathematical statements. Mathlib is a large, community-driven library built within the Lean theorem prover, a formal system that verifies every step of a mathematical proof with machine-checkable rigor. It currently contains around 105 formalized mathematical results. “Automated theorem provers are technically complex, but their development has been under-resourced,” says Sutherland. “With advances in large language models and AI, the barrier to using these tools is falling fast, making formal verification more accessible to working mathematicians.” The team’s goal is to create seamless tools that allow mathlib users to query the LMFDB directly, enabling AI agents and researchers to leverage vast amounts of unformalized mathematical knowledge without having to formalize the entire database upfront. This approach dramatically expands the scope of what can be explored during proof searches. “While proving a new theorem often requires only a small subset of known facts, the number of potential candidates for relevant information grows exponentially,” explains Roe. “By linking the LMFDB to mathlib, we can guide AI systems toward the most promising leads, accelerating discovery.” The LMFDB has already proven instrumental in major breakthroughs. For example, machine learning tools used in the study of elliptic curves helped uncover patterns in what researchers call “murmurations”—a phenomenon involving the collective behavior of number-theoretic data. The emphasis on concepts like the conductor in these databases has directly influenced such discoveries. The researchers also highlight efficiency gains: the LMFDB’s results are based on thousands of CPU-years of computation. Reusing this work avoids redundant calculations and enables faster exploration of examples and counterexamples, even when the full scope of the search is unknown. “Our next steps include assembling a dedicated team, collaborating with both the LMFDB and mathlib communities, formalizing foundational definitions related to elliptic curves, number fields, and modular forms, and building the infrastructure to run LMFDB queries directly within mathlib,” says Roe. “If you’re an MIT student interested in contributing, we encourage you to reach out.”