expMath: Exponentiating Mathematics

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.

Q1: Will expMath support systems that dynamically generate abstraction hierarchies not based in ZFC or traditional well-founded set theory—such as non-linear ordinal structures or recursion-friendly meta-models? 
A: The right way to get an answer to this kind of question is to submit an abstract. We encourage your most creative, innovative approach to solving the expMath problem.

Q2: Does the program address new math to prove performance of the compilers? 
A: The program is not focused on compilers. 

Q3: In our case we have a collaborator at a national lab who is an expert in an important part of the program/our solution. Is it possible to have that person involved with a small subaward from our institution (in this case academic institution). 
A: The structure of proposals should be in accordance with the BAA instructions. 

Q4: Do you want something aimed at mathematicians only, or are theoreticians in other fields a target audience, from fields such as physics, theoretical CS, etc? 
A: The program focuses on pure mathematics. 

Q5: Do you foresee the use of Human-studies or are you looking for mostly automated evaluation? 
A: HSR is expected only to help validate how AI is faster than humans. 

Q6: Are you expecting to make grants to successful univ applicants or will it be cooperative agreements? If the latter, can you please provide additional information about the information needed regarding project personnel? 
A: Grants are not an approved award instrument. Please refer to the BAA Overview Information section for the available types of award instruments. 

Q7: Should we include HSR to validate the results of our solutions? If so, should such human subjects be professional mathematicians? 
A: DARPA expects HSR for the TA2 evaluations. Human subjects should be at least at the level of math graduate students or above. 

Q8: Is studying the collaborative dynamics between the human subjects (mathematicians) and the AI system(s) in scope? 
A: We are not studying collaborative dynamics. HSR is relevant for validating that AI is faster than humans. 

Q9: Should proposers choose specific classes or domains of math problems to address, or will they be supplied by the program, or should solutions be directed to apply to any (professional level) problem? 
A: Propose whatever innovative solution you think is necessary. 

Q10: Are there any restrictions on the types or families of AI systems that can be used (e.g., DeepSeek)? 
A: Diverse families of AI systems may be used. 

Q11: Is there a planned down select? 
A: There is no planned down select. 

Q12: Are multiple TA2 awards planned? 
A: No specific number of TA2 awards is anticipated. 

Q13: Is prior work or experience, evidenced by research papers or products, on AI for math proofs required, or taken as an advantage for the proposal? 
A: Proposals will be evaluated in accordance with the BAA evaluation criteria. 

Q14: How important is preliminary work in the space of AI + math? For example, if someone is an expert in AI and reasoning, but not too much prior work in AI for math. 
A: We encourage you to build a team with expertise in both areas to address the BAA.

Q15: For TA2, is it more emphasized on formal mathematical background than AI? 
A: Please refer to the requirements for TA2 in the BAA on release. 

Q16: Besides PIs and co-PIs as main contributors to the project, can we include consultants who do not take big budgets but can be helpful in providing insights throughout the project? If so, what is the formal role in the DARPA contract? 
A: Yes. The formal role would be consultants, and the associated proposed cost will be evaluated as an other direct cost (ODC). 

Q17: Will applications to other domains such as software verification be considered for evaluation of program techniques? As part of proposal evaluation? 
A: No. 

Q18: What is the role of conjecture formation in expMath? 
A: Please refer to the proposer’s day video. 

Q19: Will there be datasets provided for training and validation? 
A: TA1 must get their own data for training and internal evaluation, TA2 will evaluate TA1 approaches based on their own data. 

Q20: Is any budgeting info provided? Approx. costs and how many teams funded? 
A: No, budgets should be commensurate with the scale of the effort, if one is concerned, one should align budgets and tasks closely. 

Q21: You stated that evaluations are desired for performance on professional-level math. How broadly defined is this? e.g. Applied math, stats, math phys? 
A: Pure math (proof-based).

Q22: Do we make a proposal for both decomp+auto(in)formalization? Or just one of these (TA1)? Or an option for either? 
A: Partial solutions may be considered for TA1 if they are exceptional. But proposals should address all requirements of the TA. 

Q23: How much/how early in the program (if any) is HSR expected from TA1 performers? 
A: HSR is necessary to meet the speed metric; the sooner the better, ideally within one year. 

Q24: How large is the expected team? Couple of researchers or multi-institutional? 
A: Teams should be organized to optimally deliver innovative, achievable, feasible, and complete solutions. We will consider teams of varying sizes. 

Q25: Are you interested in the impact this will have beyond mathematics, into applications in science, tech, eng., bus., software, etc.? 
A: This program focuses on pure math. 

Q26: When we examine LLM for abstraction for math problem solving, are we looking for white-box approaches or developing a better version of current LLM that can solve math problems without substantial grounding? 
A: Please refer to the BAA on release. 

Q27: Your CMO explicitly discouraged FFRDCs from proposing. What are our chances of meeting the minimum requirements for an exception? Would it be worth us submitting an abstract? We have ORNL-unique capabilities we could bring to bear on the topic and world-class experience in specific application areas such as quantum, symbolic mathematics, and software correctness with Rust and other tools. 
A: UARCs and FFRDCs interested in this solicitation, either as a prime or a subcontractor, must contact the Agency Point of Contact (POC) listed in the Overview section prior to the proposal (or abstract) due date to discuss potential participation as part of the government team or eligibility as a technical performer. 

Q28: I’d like to know your preference regarding the ambition of the proposal. Is it more important that the proposed project is feasible and has a clear path forward or that it is ambitious? 
A: Feasibility is a metric that proposals will be evaluated on. The proposal should be both. 

Q29: How important is it that tools be designed for human-in-the-loop vs fully automated? 
A: TA2 evaluations will focus on fully automated systems. 

Q30: Are UK participants eligible? 
A: In accordance with Section VII, Special Considerations – “All responsible sources capable of satisfying the Government's needs, including both U.S. and non-U.S. sources, may submit a proposal that shall be considered by DARPA.” …. “Non-U.S. organizations and/or individuals may participate to the extent that such participants comply with any necessary nondisclosure agreements, security regulations, export control laws, and other governing statutes applicable under the circumstances.”

Q31: Q: Are there are any specific requirements or documents that should be provided for the collaborators/participants/subawardees from non-U.S. institutions. Are there any citizenship considerations or documents required? 
A: Please see expMath BAA (HR001125S0010) Section VII: Special Considerations, bullet 2 which addresses the allowance of Non-U.S. Organizations and/or individuals, specifically that non-U.S. organizations and/or individuals should be able to comply with “nondisclosure agreements, security regulations, export control laws, and other governing statutes applicable under the circumstances.” Additionally, in accordance with P2 Proposal Instructions and Volume II Template (Cost) Section 9, Subawardee Costs “must be prepared at the same level of detail as that required of the prime proposer.” Lastly, please note several Subawardee requirements stated in P1 Proposal Instructions and Volume 1 Template Technical and Management. To that end, the Government recommends proposers provide information as requested and any additional information, as made allowable under the solicitation, that may allow the government to discern compliance with the aforementioned instructions. 

Q32: Open-Source Alignment: The solicitation states that "Intellectual property (IP) rights asserted by proposers are highly encouraged to align with opensource regimes." Given our need to maintain at least a held-out test set, and possibly ensuring the full question set remains closed to maintain assessment validity: 

1. Would a hybrid approach be acceptable, where methodology and infrastructure are open-sourced, while some or all evaluation questions remain proprietary?
2. Can proposers justify selective IP protection for specific deliverables based on scientific validity concerns (avoiding data contamination)? IP Evaluation Criteria: The evaluation criteria mention considering "the extent to which the proposed intellectual property rights allow the mathematics and AI community to further research and development."
3. How is this criterion weighted against the need for rigorous, contamination-free benchmarks?
4. Would a phased release strategy (immediate methodology release, delayed question release) satisfy this requirement? 

A: In accordance with Section II, Open-Source Methodology and Software, “The program places a strong emphasis on creating and leveraging open-source development, along with advocating the use of liberal open-source licensing (e.g., Apache, MIT).” Proposers who choose to assert restrictions on IP are highly encouraged to provide a comprehensive explanation of the IP approach, to include details specific to meeting the program’s goals of collaboration and broad software usability. 

Q33: Is it appropriate to buy a GPU server that will be used for the project? 
A: Unless stated in the solicitation, DARPA is unable to provide guidance on the proposer’s technical or cost approach. 

Q34: I am submitting with colleagues in another institution. Is there a preference in submitting through main organization (where I will be at), or the first institution? 
A: DARPA does not have a preference on the prime proposer; however, if you are the proposing Principal Investigator you should submit under the University you work for.

Q35: What budget constraints or expectations are there? 
A: DARPA is unable to provide further guidance on your budget approach. You should submit a budget that is reflective of your technical approach. 

Q36: Instructions in the template P3_- _Proposal_Summary_Slide_Instructions_and_Template.pptx state that “All submissions must be written in English, and all pages shall be formatted for printing on 8-1/2 by 11- inch paper with 1-inch margins and font size no smaller than 12-point. Font sizes of 8 or 10-point may be used for figures, tables, and charts. The slide in the template file is 8.5 x 14. 

1. Could the Government please clarify if offerors should use the slide size of 8.5 x 14 or the size in the instructions?
2. Will the Government provide a revised template or can offerors modify the template based on the Government’s response.
3. Could the Government kindly advise if there is a page limitation? 

A: 

1. The Proposal Summary Slide must be submitted as a standard Microsoft PowerPoint slide, and use of the provided template is strongly encouraged.
2. A revised template will not be provided. The Proposal Summary Slide must be submitted as a standard Microsoft PowerPoint slide, and use of the provided template is strongly encouraged.
3. The Proposal Summary Slide must include all components and must be submitted in Microsoft PowerPoint format under the file naming convention “Organization_Proposal Summary Slide”. Use of the provided template is strongly encouraged. No page limit is stated for the Proposal Summary Slide. 

Q37: The “Proposal Instructions and Volume II Template (Cost)” indicates that offerors must provide supporting documentation including a “Government-issued (i.e., DCMA, DCAA, ONR, etc.) Forward Pricing Rate Recommendation (FPRR) or Forward Pricing Rate Agreement (FPRA).” The Government-issued documentation is on letterhead with Controlled Unclassified Information (CUI) labels, requiring offerors to pass through the CUI designation with encryption to safeguard the CUI in accordance with 32 CFR Part 2002.14 (C). Could you please advise if the Broad Agency Announcement Tool (BAAT) is a method of secure transmission that accepts CUI documentation? If not, could you kindly advise if offerors may email the documentation separately as a password-protected file?
A: Yes, DARPA’s Broad Agency Announcement Tool (BAAT) is a method of secure transmission for CUI documentation. 

Q38: In the “P4_-_DARPA_Standard_Cost_Proposal_Spreadsheet.xlsx”, (Base, O-I, O-II, O-III, O-IV and O-V) has 6 columns representing fiscal year (FY1, FY2... FY6). Could the Government please clarify the need for these extra fiscal year columns in each tab? 
A: Please review the “General” tab in P4 – DARPA Standard Cost Proposal Spreadsheet for instructions: Enter the proposed costs detail for the Base and each Option period (as needed) on the tab entitled, “Base”, “O-I”, “O-II”, O-IV”, and “O-V”. The tab entitled, “Total Amount” will automatically calculate from the Base and Option tabs. Additional instructions on how to utilize P4 – DARPA Standard Cost Proposal Spreadsheet can be found on the “Instructions” tab. 

Q39: HR001125S0010-Amendment, Page 8, states that “The expMath program is comprised of a single, thirty-six (36)-month period of performance. Progress will be evaluated every six (6) months.” However, “P4_- _DARPA_Standard_Cost_Proposal_Spreadsheet.xlsx”, includes has a Base and five option tabs (Base, O-I, O-II, O-III, O-IV and O-V). Could the Government please clarify the reason for the additional tabs? 
A: Please review the “General” tab in P4 – DARPA Standard Cost Proposal Spreadsheet for instructions: Enter the proposed costs detail for the Base and each Option period (as needed) on the tab entitled, “Base”, “O-I”, “O-II”, O-IV”, and “O-V”. The tab entitled, “Total Amount” will automatically calculate from the Base and Option tabs. Additional instructions on how to utilize P4 – DARPA Standard Cost Proposal Spreadsheet can be found on the “Instructions” tab.