expMath

Mathematics is the source of significant technological advances. However, progress in math is slow for two primary reasons.

1. Decomposing problems into useful lemmas is a laborious and manual process. To advance the field of mathematics, mathematicians use their knowledge and experience to explore candidate lemmas, which, when composed together, prove theorems. Ideally, these lemmas are generalizable beyond the specifics of the current problem so they can be easily understood and ported to new contexts.
2. Proving candidate lemmas is slow, effortful, and iterative. Putative proofs may have gaps, such as the one in Wiles’ original proof of Fermat’s last theorem, which necessitated more than a year of additional work to fix. In theory, formalization in programming languages, such as Lean, could help automate proofs, but translation from math to code and back remains exceedingly difficult.

Recent advances in artificial intelligence (AI) suggest the possibility of increasing the rate of progress in mathematics. Still, a wide gap exists between state-of-the-art AI capabilities and pure mathematics research.

The goal of Exponentiating Mathematics (expMath) is to radically accelerate the rate of progress in pure mathematics by developing an AI co-author capable of proposing and proving useful abstractions.

expMath will comprise teams focused on developing AI capable of auto decomposition and auto(in)formalization and teams focused on evaluation with respect to professional-level mathematics. We will robustly engage with the math and AI communities toward fundamentally reshaping the practice of mathematics by mathematicians.

Kickoff

DARPA hosted the expMath kickoff event from March 2025 in Arlington, Virginia. expMath brings together an interdisciplinary community across industry, academia, and U.S. government towards enabling new mathematical discoveries and creating more rigorous foundations for – and possibilities in – AI. The program convened more than 130 attendees, including Fields medalists, Turing Award winners, and experts in mathematics and AI, for the kickoff.

The videos below feature presentations and discussions from the event, including an expMath overview provided by DARPA Program Manager Patrick Shafto. The videos also share complementary approaches from industry and their capabilities relevant to the expMath community.