Exponentiating mathematics (expmath)

The Defense Advanced Research Projects Agency awarded The Johns Hopkins University a cooperative agreement totaling $942,857.42 on March 17, 2026, under the Research and Technology Development program (CFDA 12.910) to support the Exponentiating Mathematics (EXPMATH) project. Performance runs through March 19, 2029, with work performed in Maryland.

EXPMATH pioneers the use of artificial intelligence in synthetic mathematics by developing a tool capable of formalizing homotopy type theory in Agda. The project operates as a multi-institutional collaboration with two sub-recipients. The University of Illinois, awarded $942,857.42 on September 2, 2026, is developing a model for autoformalization of natural language into Agda code and integrating that model with other project components; deliverables include code, models, and open-source reports on results. The University of Massachusetts, awarded on August 17, 2026, is developing a model for autodecomposition of natural language and Agda and collaborating with other teams on model integration; deliverables similarly comprise code, models, and open-source technical reports.

The Research and Technology Development program funds basic, applied, and advanced research with potential military or dual-use application at educational institutions, nonprofits, and commercial firms, with awards based on competitive scientific review and evaluated on overall scientific and technical merit, relevance to DARPA mission, recipient capabilities, technology transition plans, and cost realism.