HR001125S0010-Amendment-01.pdf

This publication constitutes a Broad Agency Announcement (BAA) as contemplated in Federal Acquisition Regulation (FAR) 6.102(d)(2) and 35.016 and 2 CFR § 200.203. Any resultant award negotiations will follow all pertinent law and regulation, and any negotiations and/or awards for procurement contracts will use procedures under FAR 15.4, Contract Pricing, as specified in the BAA.

Broad Agency Announcement Information Innovation Office

Exponentiating Mathematics (expMath)

HR001125S0010

March 03, 2025

AMENDMENT 1

HR001125S0010

HR001125S0010 AMENDMENT 1

Changes Made

Language has been added to Section I: Overview Information to provide details on where to access published Frequently Asked Questions (FAQs) documents for the expMath program.

Language has been added to Section VII: Special Considerations regarding Human Subjects Research.

All changes are highlighted in yellow.

SECTION I: OVERVIEW INFORMATION

Federal Agency Name – Defense Advanced Research Projects Agency (DARPA), Information Innovation Office (I2O)

Funding Opportunity Title – Exponentiating Mathematics (expMath)

Announcement Type – Amendment

Funding Opportunity Number – HR001125S0010

Assistance Listing Number: 12.910

Dates/Time - All Times are Eastern Time Zone (ET) o Posting Date: March 03, 2025 o Proposers Day: April 23, 2025 o Proposal Abstract Due Date: May 15, 2025 at 5:00 PM o Question Submittal Closed: June 25, 2025 at 5:00 PM o Proposal Due Date: July 8, 2025 at 5:00 PM

Anticipated Individual Awards - Multiple awards are anticipated.

Types of Instruments that may be Awarded – Procurement Contract, Cooperative Agreement, Other Transactions for Prototype, or Other Transactions for Research

NAICS Code: 541715

Agency contact

The BAA Coordinator for this effort may be reached at: expMath@darpa.mil

DARPA/ I2O

ATTN: HR001125S0010

675 North Randolph Street Arlington, VA 22203-2114

Frequently Asked Questions (FAQs) will be published on the expMath program page at:

https://www.darpa.mil/research/programs/expmath-exponential-mathematics https://www.darpa.mil/research/programs/expmath-exponential-mathematics

SECTION II: FUNDING OPPORTUNITY DESCRIPTION

The Defense Advanced Research Projects Agency (DARPA) is soliciting innovative proposals in the technical area of artificial intelligence (AI) to dramatically increase the rate of progress in mathematics. Proposed research should investigate innovative approaches that enable revolutionary advances in science, devices, or systems. Specifically excluded is research that primarily results in evolutionary improvements to the existing state of practice.

Program Goal

The Exponentiating Mathematics (expMath) program aims to develop an AI collaborator to increase the rate of progress in mathematics by orders of magnitude. The program will also aim to develop new evaluation methods to assess the progress of AI systems towards professional mathematics.

Program Background

Mathematics is the source of the most transformative technological advances1, but progress in mathematics is slow. Improved understanding, not mere technical correctness, drives mathematics forward. Advances in AI for mathematics require fundamental advances in abstractions that support generalization (i.e. lemmas). These advances go beyond statistical approaches in current language models and beyond syntactic correctness in proof checking.

Accelerating the speed of mathematicians and mathematics will require a commitment to rigorously understanding and addressing the problem of abstraction that the tech community has eschewed in favor of purely statistical approaches.

Advances in mathematics are slow for several reasons, two of which are especially challenging.

First, the decomposition of problems into useful lemmas2 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 current problem's specifics so they can be easily understood and ported to new contexts.

Second, proving candidate lemmas is slow, effortful, and iterative. Putative proofs may have gaps, such as in Wiles’ original proof of Fermat’s last theorem, which necessitated more than a year of additional work to correct. In theory, formalization in programming languages, such as Lean may aid in proof automation. However, translating between mathematics expressed in natural language and theorem prover code remains exceedingly difficult.

Although AI is being explored for math, current efforts are (1) aimed at the International Math Olympiad (IMO) level3,4,5,6 rather than professional mathematics and (2) not focused on the central role of abstraction in mathematics. Uniquely, expMath focuses on advancing pure mathematics by mathematicians to fundamentally change the practice of mathematics and radically increase productivity.

Program Introduction expMath hypothesizes that automating abstraction will increase the rate of progress in mathematics by orders of magnitude. The program seeks to address the two challenges above by developing new methods for (1) autodecomposition of a given problem into collections of lemmas and (2) auto(in)formalization for going back and forth between natural language statements of lemmas and an automated theorem proving language.

This solicitation seeks methods that go beyond recent advances in AI and automated mathematics. Existing research in AI has demonstrated successful translations between written languages7 and generative capabilities for code.8 There is modest but growing interest in AI and formal methods within the mathematics community. Multiple proof assistant frameworks are being developed by mathematicians (e.g. Lean9, Isabelle10). Three Fields’ medalists11,12 are advocating for leveraging AI and formal methods in their breakthroughs,13 but efforts to date have focused on literature search and checking correctness rather than ideation. Moreover, recent AI-assisted work in specialized fields has resulted in published papers,14,15,16 though the approaches have been exceptionally manual and hence, do not scale. 17 Recent research has separately suggested tree and program search for automated proofs,18,19 expert iteration for math curriculum learning,20 and chain-of-thought reasoning for policy improvement21 for IMO (high-school) level problems. A parallel line of research has suggested viewing math via procedural abstraction to define and compose search problems, but without autoformalization or search.22 Recent work by Google has succeeded at geometry for IMO problems without human labeled data.23

National Security Impact

To ensure the United States’ continued technological leadership, it is necessary to innovate in the practice of mathematics, leveraging U.S. leadership in AI. Moreover, we may not have decades to address many of the hard problems that have fundamental mathematical challenges at their core. These hard problems include faster algorithms for factoring semiprimes; more precise and efficient climate models; faster, safer, and more effective AI algorithms; effective quantum computing; understanding of robustness and failure points of ecological systems and food security; and scalable theoretical models of cybersecurity. Further, AI models that can provably enforce consistency with natural language documentation are necessary in adhering to manufacturing, legal, and ethical requirements, as well as for meeting requirements of software.

Program Structure

The expMath program will be comprised of two technical areas (TAs). TA1 will focus on automation of decomposition and formalization/informalization. TA2 will focus on evaluation of progress relative to professional mathematics, as represented by research papers and graduate level textbooks.

Proposers may submit against either TA. Proposers may submit against both TAs, though two separate proposals must be submitted, one addressing TA1 and the other addressing TA2; a single proposal received addressing both TAs will be found non-conforming. While organizations may submit an individual proposal against both TAs, no proposer, whether prime or subcontractor, will be selected to perform on more than one TA.

Proposals addressing TA1 are expected to have strong expertise in both mathematics and AI.

Proposals addressing TA2 are expected to have strong expertise in both designing evaluations of AI technologies and mathematics.

TA1 Automation: The goal of TA1 is to develop technologies for AI collaborators through the problems of decomposition and formalization. Decomposition is the problem of positing a collection of lemmas that, if true, prove a theorem. In professional mathematics, lemmas may be adapted from previous work or formulated as entirely new, generalizable statements. Formalization is the problem of translating from natural language to a theorem proving language (e.g. Lean) and translating the proof back to natural language. Therefore, technical approaches should build on ongoing successes in automated theorem proving. The resulting system should be able to assist mathematicians with ideation around candidate proof strategies and assist with substantiation of lemmas, all in natural language and grounded in formalized proofs.

Proposers may use any technical approach but should comprehensively (1) explain the technical approach, (2) explain how the technical approach enables rapid iteration between abstraction and code execution to accelerate progress in mathematics, and (3) demonstrate through evidence that the program metrics may be achieved through the technical approach. Potential approaches may include, but are not limited to, recursion planning24, curriculum learning25, function calls integrated into large language models (LLMs)26, program synthesis27, and meta learning28.

Additionally, TA1 performers will be required to provide the fully integrated software to TA2 performer(s) for evaluation. Thus, the proposed technical approach should clearly describe the software development plan and delivery to TA2 performer(s) for timely evaluation (est. delivery 1 month before evaluations).

TA2 Evaluation: The goal of TA2 is to develop methods for evaluating the tools developed by TA1 performers using appropriate research datasets. As detailed above, proposals addressing TA2 are expected to have strong expertise in both mathematics and designing evaluations of AI technologies.

Program evaluation will be conducted every six months. To demonstrate impact, evaluations will be conducted in diverse areas of mathematics, as well as across levels of expertise. While the broadest possible coverage of mathematics is encouraged, strong TA2 proposals should specifically address three specific subfields: (1) partial differential equations (Navier Stokes), (2) number theory (Reimann Hypothesis), and (3) computational complexity (P =/≠ NP). Expertise levels will range from graduate student introductory books (such as Principles of Functional Analysis1, Number Theory2, and Theory of Computation3) to advanced level books (such as the Navier Stokes Problem in the 21st Century4, Advanced Number Theory5, and Computers and Intractability: A Guide to the Theory of NP-Completeness6). In addition, curated research papers from both general and specific areas should be employed.

TA2 teams must propose a system for evaluation of AI capabilities with respect to professional mathematics. The program envisions evaluations structured as cross-validation. For example, presented with a paper, omit one (or more) lemmas. Evaluation is based on correctly positing the lemma (or equivalent), formalizing, proving, and stating the proof in natural language. Proposers must include a plan for ensuring evaluation includes lemmas that are not in the training set. Proposers are encouraged to elaborate on this framework to maximize the effectiveness and longevity of evaluations. Strong proposals will describe how the proposed systems will be made available and will be easily usable beyond the program.

Program Metrics

Program success will be measured against progress in automation and speed, as illustrated in Figure 1. The goal of TA1 is to correctly predict and prove lemmas in 90% of evaluation problems and demonstrate a 100x reduction in solution time as compared to solutions as repeated by a graduate student by hand. The goal of TA2 is to optimize efficiency as measured by precision of estimation per unit of resource.

Figure 1: Program Metrics

1 Schechter, M. (2002) Principles of functional analysis Vol 36. Providence, RI: American Mathematical Society (Graduate Studies in Mathematics).

2 Neukirch, J. (1999) Algebraic number theory Vol 322. Springer International Publishing (Grundlehren der mathematischen Wissenschaften).

3 Sipser, M. (1996). Introduction to the Theory of Computation. ACM Sigact News, 27(1), 27-29.

4 Lemarie-Rieusset, P.G. (2016). The Navier-Stokes Problem in the 21st Century (1st ed.). Chapman and Hall/CRC.

5 Cohn, H. (1980). Advanced number theory. Courier Corporation.

6 Garey, M. R.; Johnson, D. S. (1979). Victor Klee (ed.). Computers and Intractability: A Guide to the Theory of NP-Completeness. A Series of Books in the Mathematical Sciences. San Francisco, Calif.: W. H. Freeman and Co.

As stated above, TA1 proposals should clearly and completely demonstrate through evidence that the program metrics may be achieved through the proposed technical approach. TA2 proposals should clearly describe how their system is efficient in evaluating for the above metrics.

Program Schedule

The expMath program is comprised of a single, thirty-six (36)-month period of performance.

Progress will be evaluated every six (6) months. Proposals should include a detailed schedule of logically sequenced tasks/subtasks, as well as metrics and milestones every twelve (12) months.

These items should progressively and in sum constitute a constructive plan for achieving the proposed technical objectives while appropriately managing risk. For budgeting purposes, use January 1, 2026, as a start date for both TAs.

The Government will specify the locations for Principal Investigator (PI) meetings during program performance. PI meetings will be held approximately every six (6) months, the first of which will serve as a program kickoff. For travel planning and costing, assume six (6) trips during the period of performance of the program schedule illustrated in Figure 2, alternating between Washington, DC and San Diego, CA, with each trip requiring two (2)-days and three (3)-nights. Proposers should ensure budgets reflect sufficient funds for key technical personnel who will most directly contribute to the meetings. At the meetings, PIs will present new research findings and accomplishments, review results of evaluations, review plans for the next period, discuss implementation milestones, and resolve any programmatic, budget, and/or logistical issues. In addition to PI meetings, the Government team will conduct site visits and hold monthly teleconference meetings with each PI and their team.

Figure 2: Program Schedule

Additionally, proposers (prime and subcontractor) who plan to propose travel for conferences should describe why attendance at the conference(s) will benefit the project and how the proposer will mitigate cost and schedule impacts to the expMath program.

Further, the Government expects all performers to collaborate between teams and across TAs.

Proposers should read the descriptions of each TA to ensure a full understanding of the program context, structure, and anticipated relationships required among performers. To facilitate the open exchange of information, all program performers will have an Associate Contractor Agreement (ACA) language included in their award.

Open-Source Methodology and Software

Intellectual property (IP) rights asserted by proposers are highly encouraged to align with open-source regimes, fostering a collaborative and transparent environment. 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). This strategy includes the establishment of open-source repositories (e.g., GitHub), which are accessible for review by the Government team, other performers, and the wider research community. Such an approach is pivotal in promoting a culture of open innovation and shared knowledge. By facilitating this openness, the program aims to spur rapid innovation and continuous improvement. Openness and transparency are achieved by providing a robust foundation for future users or developers of the program’s technologies and deliverables. Moreover, this open-source methodology ensures that the advancements and learnings are not siloed, but contributes to the collective intelligence of the field, leading to more significant and impactful technological progress.

SECTION III: EVALUATION CRITERIA

Proposals will be evaluated using the following criteria listed in descending order of importance. Overall Scientific and Technical Merit; Potential Contribution and Relevance to the DARPA Mission; and Cost Realism.

o Overall Scientific and Technical Merit: The proposed technical approach is innovative, feasible, achievable, and complete. The proposed technical team demonstrated expertise and experience to accomplish the proposed technical approach. The proposal provides a detailed technical rationale demonstrating that the technical approach can achieve the program goals, schedule, and metrics. The proposal clearly identifies major technical risks and planned mitigation efforts that are defined and feasible.

o Potential Contribution and Relevance to the DARPA Mission: The potential contributions of the proposed effort bolster the national security technology base and support DARPA’s mission to make pivotal early technology investments that create or prevent technological surprise. In addition, the evaluation will take into consideration the extent to which the proposed intellectual property rights allow the mathematics and AI community to further research and development in this domain.

o Cost Realism: The proposed costs are realistic for the technical and management approach and accurately reflect the technical goals and objectives of the solicitation. The proposed costs are consistent with the proposer's Statement of Work and reflect a sufficient understanding of the costs and level of effort needed to successfully accomplish the proposed technical approach. The costs for the prime proposer and proposed sub-awardees are substantiated by the details provided in the proposal (e.g., the type and number of labor hours proposed per task, the types and quantities of materials, equipment and fabrication costs, travel and any other applicable costs and the basis for the estimates). The proposed costs leverage all available relevant prior research and development that may reduce initial development costs.

Unless otherwise specified in this announcement, for additional information on how DARPA reviews and evaluates proposals through the Scientific Review Process, please visit: Proposer Instructions: General Terms and Conditions.

https://www.darpa.mil/work-with-us/proposer-instructions

SECTION IV: ABSTRACT GUIDELINES

This announcement contains an abstract phase. Proposers are strongly encouraged to submit an abstract in advance of a full proposal submission to minimize effort and reduce the potential expense of preparing an out-of-scope proposal; however, submission of an abstract is not required.

Abstract Content

Abstract content and formatting requirements are stated in the Abstract Instructions and Submission Template and the Abstract Summary Slide Template found in the Abstract Attachments (A-1 and A-2). All abstracts submitted in response to this solicitation must comply with the content and formatting requirements stated in the aforementioned attachments. Use of the Abstract Templates is required in the development of abstract submissions. Information not explicitly requested in this solicitation and the abstract attachments may not be reviewed.

Abstract Submission Requirements:

The Abstract submission deadline is as stated in Section I: Overview Information.

Abstracts must be submitted to the DARPA Broad Agency Announcement Tool (BAAT).

Please visit Proposer Instructions and General Terms and Conditions for specific information regarding submission methods through BAAT. Submissions sent through other mediums, channels, or after the prescribed deadline will not be accepted.

Proposers are responsible for clearly identifying proprietary information on the Abstract cover page. Marking must state, “Proprietary.” Note, “confidential” is not a classification marking used to control the dissemination of U.S. Government National Security Information as dictated in Executive Order 13526 and should not be used to identify proprietary business information.

Abstract Feedback:

DARPA will review abstracts for conformance; only conforming abstracts will be reviewed and receive feedback.

All conforming abstracts will receive written feedback either encouraging or discouraging a full proposal submission. The Government’s feedback determination will be accompanied by a brief technical analysis which resulted in the feedback response. Feedback will be sent to the administrative and technical points of contact noted on the abstract cover page.

Regardless of DARPA’s response to an abstract, proposers may submit a full proposal.

Without regard to any comments or feedback resulting from the review of an abstract, DARPA will review all conforming full proposals using the published evaluation criteria.

SECTION V: PROPOSAL GUIDELINES

Proposal Preparation Requirements

All proposers must be registered in the System for Award Management (SAM) and have a Unique Entity Identifier (UEI) number for their proposal to be found conforming. Proposers must maintain an active registration in SAM.gov with current information at all times during which a proposal is under consideration or have a current award with DARPA. Information on SAM registration is available at SAM.gov.

NOTE: New registration takes an average of 7-10 business days to process in SAM.gov.

Registration requires at a minimum the following information:

SAM UEI number.

Tax Identification Number.

Commercial and Government Entity (CAGE) Code. If a proposer does not already have a CAGE code, one will be assigned during the SAM registration process.

Electronic Funds Transfer information (e.g., proposer’s bank account number, routing number, and bank phone or fax number).

Proposal Content

This announcement allows for multiple award instrument types to include Procurement Contracts, Other Transactions, and Cooperative Agreements. Some award instrument types have specific cost-sharing requirements. All proposals submitted in response to this announcement must comply with the content and formatting requirements stated in the Proposal Attachments.

Proposers are required to use the templates provided; information not explicitly requested in this announcement or the Attachments, may not be evaluated.

SECTION VI: SUBMISSION INFORMATION

This announcement allows for multiple award instrument types to be awarded to include

Procurement Contracts, Cooperative Agreements, and Other Transactions. Some award instrument types have specific cost-sharing requirements. The following websites are incorporated by reference and contain additional information regarding overall proposer instructions, general terms and conditions, and each specific award instrument type.

Proposers must review the following links:

o Proposer Instructions: General Terms and Conditions: https://www.darpa.mil/work-with-us/proposer-instructions o Procurement Contracts: https://www.darpa.mil/work-with-us/procurement-contracts o Assistance (Cooperative Agreements): https://www.darpa.mil/work-with-us/grant-cooperative-agreements o Other Transaction agreements: https://www.darpa.mil/work-with-us/other-transaction-agreements

This announcement contains an abstract phase. Abstracts are strongly encouraged but not required. Abstracts are due on the date and time stated in Section I, Overview. Additional instructions for abstract submission are contained within the Abstract Attachments.

Abstract Attachments o (required) A1 Abstract Instructions and Submission Template o (required) A2 Abstract Summary Slide Instructions and Template

Full proposals are due on the date and time stated in Section I, Overview. The Proposal Attachments contain specific instructions and templates and constitute a full proposal submission. Please visit Proposer Instructions and General Terms and Conditions for specific information regarding submission methods through the Broad Agency Announcement Tool

(BAAT).

Proposal Attachments:

o (required) P1: Proposal Instructions and Volume I Template (Technical and

Management) o (required) P2: Proposal Instructions and Volume II Template (Cost) o (required) P3: Proposal Summary Slide Template o (required) P4: DARPA Standard Cost Proposal Spreadsheet o (informational only) P5: Associate Contractor Agreement (ACA)

Baseline Model Contracts, Other Transactions, and Cooperative Agreements are attached to this solicitation. Redline edits to the corresponding Baseline Model should be submitted with the proposal.

Baseline Model Contracts: For informational purposes only o Baseline Model-Contract Large Business o Baseline Model-Contract Small Business o Baseline Model-Contract Addendum Circumstance-Driven Additional Clauses o Baseline Model-Cooperative Agreement https://www.darpa.mil/work-with-us/grant-cooperative-agreements o Baseline Model-OT P-Fixed Support Nontraditional o Baseline Model-OT R-Fixed Support Company

SECTION VII: SPECIAL CONSIDERATIONS

This announcement, stated attachments, and websites incorporated by reference constitute the entire solicitation. In the event of a discrepancy between the announcement, attachments, or websites, the announcement takes precedence.

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.

Historically Black Colleges and Universities, Small Businesses, Small Disadvantaged Businesses and Minority Institutions are encouraged to submit proposals and join others in submitting proposals; however, no portion of this announcement will be set aside for these organizations’ participation due to the impracticality of reserving discrete or severable areas of this research for exclusive competition among these entities. 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.

As of the time of publication of this solicitation, no proposal will be accepted that is classified. All proposal submissions are expected to be unclassified. Program work is expected to be unclassified.

This program is subject to an Associate Contractor Agreement. An ACA is an agreement between non-Federal entities of Federal contractors (hereinafter contractor) working in furtherance of the DARPA agreement that requires the parties to share information, data, technical knowledge, expertise, or resources. An Associate Contractor is defined as a party to an ACA. DARPA is not a party to an ACA.

DARPA has utilized an alternate structured approach for the determination of a reasonable fee basis for Cost-Plus-Fixed-Fee (CPFF) procurement contracts under expMath, in accordance with DFARS 215.404-4(b)(1)(C). The fee calculation percentage range determined reasonable for procurement contract awards under expMath is 6.0% - 9.0%. This was determined based on consideration of factors such as: performance risk; contract type risk; facilities capital employed; anticipated award size; available transition path; markets (commercial, Government, international); IP rights; chances of award; time to production;

and solicitation complexity. Proposers should propose a fee that falls within the above range.

Because that fee range already has been determined to be reasonable relative to expMath, proposals need not include any further fee justification. Elimination of the fee as a negotiation item is expected to result in reduced contracting timelines for any proposal selected for award negotiation. It should be noted that this structured approach may not apply to other transactions requested by non-traditional defense contractors.

DARPA encourages technical solutions from all responsible sources capable of satisfying the government’s needs. To ensure fair competition across the ecosystem, DARPA prohibits contractors/performers from concurrently providing Systems Engineering Technical Assistance (SETA), Advisory and Assistance Services (A&AS), or similar support services and being a technical performer, unless the DARPA Deputy Director grants a written waiver.

DARPA extends this prohibition to University-Affiliated Research Centers (UARCs) and Federally Funded Research and Development Centers (FFRDCs) including National Labs, who as a result of their specialized expertise and areas of competencies, are able to accomplish integral tasks that cannot be met by government or contractor resources.

Therefore, these entities are highly discouraged from proposing against this solicitation as award to a UARC or FFRDC will only be made by exception. 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.

As of the date of publication of this solicitation, the Government expects that program goals as described herein may be met by proposers intending to perform fundamental research and does not anticipate applying publication restrictions of any kind to individual awards for fundamental research that may result from this solicitation. Notwithstanding this statement of expectation, the Government is not prohibited from considering and selecting research proposals that, while perhaps not qualifying as fundamental research under the foregoing definition, still meet the solicitation criteria for submissions. If proposals are selected for award that offer other than a fundamental research solution, the Government will either work with the proposer to modify the proposed statement of work to bring the research back into line with fundamental research or else the proposer will agree to restrictions in order to receive an award. For additional information on fundamental research, please visit Proposer Instructions: General Terms and Conditions.

Proposals could potentially include Human Subjects Research (HSR) and/or Animal Use.

Proposers that anticipate involving human subjects or animals in the proposed research must comply with the approval procedures detailed at https://www.darpa.mil/work-with-us/humanresearch to include providing the information specified therein as required for proposal submission.

The APEX Accelerators program, formerly known as the Procurement Technical Assistance Program (PTAP), focuses on building strong, sustainable, and resilient U.S. supply chains by assisting a wide range of businesses that pursue and perform under contracts with the DoD, other federal agencies, state and local governments, and government prime contractors. See www.apexaccelerators.us/ for more information.

APEX Accelerators helps businesses:

o Complete registration with a wide range of databases necessary for them to participate in the government marketplace (e.g., SAM).

o Identify which agencies and offices may need their products or services and how to connect with buying agencies and offices.

o Determine whether they are ready for government opportunities and how to position themselves to succeed.

o Navigate solicitations and potential funding opportunities.

o Receive notifications of government contract opportunities on a regular basis.

o Network with buying officers, prime contractors, and other businesses.

o Resolve performance issues and prepare for audit, only if the service is needed, after receiving an award.

https://www.darpa.mil/work-with-us/proposer-instructions https://www.darpa.mil/work-with-us/proposer-instructions https://ddmdraft.darpa.mil/work-with-us/proposer-instructions https://www.apexaccelerators.us/

Project Spectrum is a nonprofit effort funded by the DoD Office of Small Business Programs to help educate the Defense Industrial Base (DIB) on compliance. Project Spectrum is vendor-neutral and available to assist businesses with their cybersecurity and compliance needs. Their mission is to improve cybersecurity readiness, resilience, and compliance for small/medium-sized businesses and the federal manufacturing supply chain. Project Spectrum events and programs will enhance awareness of cybersecurity threats within the manufacturing, research and development, and knowledge-based services sectors of the industrial base. Project Spectrum will leverage strategic partnerships within and outside of the DoD to accelerate the overall cybersecurity compliance of the DIB.

www.projectspectrum.io is a web portal that will provide resources such as individualized dashboards, a marketplace, and Pilot Program to help accelerate cybersecurity compliance.

DARPAConnect offers free resources to potential performers to help them navigate DARPA, including “Understanding DARPA Award Vehicles and Solicitations”, “Making the Most of Proposers Days”, and “Tips for DARPA Proposal Success”. Join DARPAConnect at www.DARPAConnect.us to leverage on-demand learning and networking resources.

DARPA has streamlined our Broad Agency Announcements and is interested in your feedback on this new format. Please send any comments to DARPAsolicitations@darpa.mil.

1 Indeed, math arguably won World War II, through the development of the atomic bomb, jet propulsion, and breaking the enigma machine, and established the US as a superpower through development of the computer and sophisticated simulation technologies.

2 Throughout we will use lemma as shorthand for intermediate-level structure including propositions and definitions.

3 Imani, S., Du, L., & Shrivastava, H. (2023). Mathprompter: Mathematical reasoning using large language models. arXiv preprint arXiv:2303.05398.

4 Luo, H., Sun, Q., Xu, C., Zhao, P., Lou, J., Tao, C., ... & Zhang, D. (2023). Wizardmath: Empowering mathematical reasoning for large language models via reinforced evol-instruct. arXiv preprint arXiv:2308.09583.

5 Wu, Y., Jia, F., Zhang, S., Wu, Q., Li, H., Zhu, E., ... & Wang, C. (2023). An Empirical Study on Challenging Math Problem Solving with GPT-4. arXiv preprint arXiv:2306.01337.

6 Lewkowycz, A., Andreassen, A., Dohan, D., Dyer, E., Michalewski, H., Ramasesh, V., ... & Misra, V. (2022).

Solving quantitative reasoning problems with language models. Advances in Neural Information Processing Systems, 35, 3843-3857.

7 Stahlberg, F. (2020). Neural machine translation: A review. Journal of Artificial Intelligence Research, 69, 343- 418.

8 Zaremba, Wojciech (August 10, 2021). "OpenAI Codex". OpenAI.

9 de Moura, L., Kong, S., Avigad, J., Van Doorn, F., & von Raumer, J. (2015). The Lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25 (pp. 378-388). Springer International Publishing.

10 Wenzel, M., Paulson, L. C., & Nipkow, T. (2008). The Isabelle framework. In Theorem Proving in Higher Order Logics: 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings 21 (pp.

33-38). Springer Berlin Heidelberg.

11 Personal communications with Terry Tao, Akshay Venkatesh, and Helmut Hofer.

12 Tao, Terry. (2024). Machine Assisted Proof. Lectures to be delivered at the Joint Mathematics Meetings.

https://www.jointmathematicsmeetings.org/meetings/national/jmm2023/2270_program.html 13 Hartnett, K. (2021). Proof assistant makes jump to big-league math. Online at https://www. quantamagazine.

org/lean-computer-program-confirms-peter-scholze-proof-20210728.

https://www.projectspectrum.io/ http://www.darpaconnect.us/ mailto:DARPAsolicitations@darpa.mil https://en.wikipedia.org/wiki/Wojciech_Zaremba https://openai.com/blog/openai-codex/ https://en.wikipedia.org/wiki/OpenAI

14 Davies, A., Veličković, P., Buesing, L., Blackwell, S., Zheng, D., Tomašev, N., ... & Kohli, P. (2021). Advancing mathematics by guiding human intuition with AI. Nature, 600(7887), 70-74.

15 Blundell, C., Buesing, L., Davies, A., Veličković, P., & Williamson, G. (2022). Towards combinatorial invariance for Kazhdan-Lusztig polynomials. Representation Theory of the American Mathematical Society, 26(37), 1145-1191 16 Davies, A., Juhász, A., Lackenby, M., & Tomasev, N. (2021). The signature and cusp geometry of hyperbolic knots. arXiv preprint arXiv:2111.15323 17 Personal communication with Alex Davies.

18 Lample, G., Lacroix, T., Lachaux, M. A., Rodriguez, A., Hayat, A., Lavril, T., ... & Martinet, X. (2022).

Hypertree proof search for neural theorem proving. Advances in Neural Information Processing Systems, 35, 26337- 26349.

19 Romera-Paredes, B., Barekatain, M., Novikov, A., Balog, M., Kumar, M. P., Dupont, E., ... & Fawzi, A. (2023).

Mathematical discoveries from program search with large language models. Nature, 1-3.

20 Polu, S., Han, J. M., Zheng, K., Baksys, M., Babuschkin, I., & Sutskever, I. (2022). Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344.

21 Polu, S., Han, J. M., Zheng, K., Baksys, M., Babuschkin, I., & Sutskever, I. (2022). Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344.

22 Poesia, G., & Goodman, N. D. (2023). Peano: learning formal mathematical reasoning. Philosophical Transactions of the Royal Society A, 381(2251), 20220044.

23 Trinh, T. H., Wu, Y., Le, Q. V., He, H., & Luong, T. (2024). Solving olympiad geometry without human demonstrations. Nature, 625(7995), 476-482.

24 Wang, H., Xin, H., Liu, Z., Li, W., Huang, Y., Lu, J., ... & Liang, X. (2024). Proving Theorems Recursively. arXiv preprint arXiv:2405.14414.

25 Polu, S., Han, J. M., Zheng, K., Baksys, M., Babuschkin, I., & Sutskever, I. (2022). Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344.

26 Azerbayev, Z., Schoelkopf, H., Paster, K., Santos, M. D., McAleer, S., Jiang, A. Q., ... & Welleck, S. (2023).

Llemma: An open language model for mathematics. arXiv preprint arXiv:2310.10631. Also, Gao, L., Madaan, A., Zhou, S., Alon, U., Liu, P., Yang, Y., ... & Neubig, G. (2023, July). Pal: Program-aided language models. In International Conference on Machine Learning (pp. 10764-10799). PMLR.

27 Wong, L., Grand, G., Lew, A. K., Goodman, N. D., Mansinghka, V. K., Andreas, J., & Tenenbaum, J. B. (2023).

From word models to world models: Translating from natural language to the probabilistic language of thought. arXiv preprint arXiv:2306.12672.

28 Song, P., Yang, K., & Anandkumar, A. (2024). Towards Large Language Models as Copilots for Theorem Proving in Lean. arXiv preprint arXiv:2404.12534.