Researchers consider expMath to use artificial intelligence (AI) for fundamentally reshaping mathematics
ARLINGTON, Va. – Military researchers are considering a new project to use artificial intelligence (AI) to boost research in mathematics with a goal of accelerating military technological progress.
Officials of the U.S. Defense Advanced Research Projects Agency (DARPA) in Arlington, Va., issued a future program announcement (DARPA-SN-25-41) last Friday for the future Exponentiating Mathematics (expMath) project.
Progress in pure mathematics
The goal of expMath is to accelerate the rate of progress in pure mathematics by developing an AI co-author capable of proposing and proving useful abstractions.
Mathematics is the source of significant technological advances, yet progress in math is slow, DARPA researchers say. Recent advances in 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.
Advances in mathematics are slow for two reasons. First, 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.
Slow and difficult
Second, proving candidate lemmas is slow, effortful, and iterative. Putative proofs may have gaps, such as the one in Wiles’s 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.
The significant recent advances in AI fall short of the automated decomposition or auto(in)formalization challenges. Decomposition in formal settings is a manual process, with existing tools like Blueprint for Lean only facilitate the structuring of math and code.
Auto(in)formalization is an active area of research in the AI literature, but current approaches show poor performance and have not yet advanced to even graduate-level textbook problems.
Formal languages
Formal languages with automated theorem-proving tools, such as Lean and Isabelle, have traction in the community for problems where the investment in manual formalization is worth it.
The expMath project will be composed of teams focused on developing AI capable of auto decomposition and auto(in)formalization and teams focused on evaluating professional-level mathematics, with a goal of fundamentally reshaping the practice of mathematics by mathematicians.
This is not a formal solicitation for proposals, and is intended only for planning. Email questions or concerns to DARPA at [email protected]. More information is online at https://sam.gov/opp/4def3c13ca3947069b1779e7ff697c6a/view.
John Keller | Editor-in-Chief
John Keller is the Editor-in-Chief, Military & Aerospace Electronics Magazine--provides extensive coverage and analysis of enabling electronics and optoelectronic technologies in military, space and commercial aviation applications. John has been a member of the Military & Aerospace Electronics staff since 1989 and chief editor since 1995.
