Image Courtesy of DARPA expMath webpage.
UCLA recently signed a $5 Million Dollar Contract with the Defense Advanced Research Projects Agency (DARPA) for the expMath: Exponentiating Mathematics initiative. Professors Wei Wang, Andrea Bertozzi, Terence Tao, Kai-Wei Chang, Nanyun Peng, and Amit Sahai are involved in this effort led by PI Wei Wang.
Exponentiating Mathematics (expMath) was created to accelerate the progress of pure mathematics by developing an AI co-author capable of proposing and proving useful abstractions. expMath has recruited teams from various institutions to focus on developing AI capable of auto decomposition, autoformalization, and evaluation with respect to professional-level mathematics. This program builds on prior work, including that of Professor Terence Tao on formalizing mathematical arguments in the proof assistant language Lean.
Response from Professor Terence Tao
“I’m excited to be working with Andrea and my CS colleagues on how to combine modern AI tools, knowledge graph representations, and formal verification to meet the DARPA challenge of automatically decomposing and then formalizing mathematical proofs at scale, which could potentially generate many new ways we can use the mathematical literature. Definitely a different type of project than the pure math projects I am more accustomed to!”
The Defense Advanced Research Projects Agency (DARPA) is an independent research and development agency within the U.S. Department of War (DoW).
Learn more about the DARPA ExpMath here.
Watch the DARPA ExpMath introduction video here.
