NSF Research: Artificial Intelligence, Formal Methods, and Mathematical Reasoning

The National Science Foundation (NSF), an independent federal agency established by the National Science Foundation Act of 1950, aims to promote the progress of science and advance national welfare through education and research support. With oversight from the Directorates for Mathematical and Physical Sciences (MPS) and Computer and Information Science and Engineering (CISE), NSF is currently offering the Artificial Intelligence, Formal Methods, and Mathematical Reasoning (AIMing) grant. This initiative seeks to fund interdisciplinary research that integrates artificial intelligence (AI), formal methods, and mathematical reasoning to advance machine-assisted mathematical discovery and understanding. The AIMing program supports innovative projects that lie at the intersection of computational and AI technologies and mathematical strategies to facilitate automated knowledge discovery. Recognizing the emerging impact of machine-assisted reasoning tools such as interactive theorem provers and AI-driven verification systems, the program encourages efforts that enhance both mathematical and computational models. The scope of supported projects includes, but is not limited to, developing AI for mathematical proof generation, advancing formal methods and theorem provers, and creating training datasets for mathematical reasoning under certainty and uncertainty. Eligibility for this grant includes U.S.-based accredited institutions of higher education and non-profit, non-academic organizations directly involved in research or education. All PIs, co-PIs, or key personnel must hold tenured, tenure-track, or equivalent full-time research positions at eligible U.S. campuses. Each eligible individual may only submit or participate in one proposal per cycle. No organizational limits are imposed on the number of submissions. Applications must be submitted through either Research.gov or Grants.gov and should comply with the guidelines specified in the NSF Proposal and Award Policies and Procedures Guide. Proposals are reviewed based on NSF’s standard merit review criteria, emphasizing intellectual merit and broader impacts, as well as specific collaboration plans and computational and mathematical innovation. Although letters of intent and preliminary proposals are not required, full proposals must begin with “AIMing:” in their titles and budget for annual PI meetings. The funding ranges from $500,000 to $1.2 million per award, with a total program allocation of up to $6 million annually. Each project may span up to three years, and an estimated 6 to 10 projects will be funded each competition cycle. No cost-sharing or matching funds are required. Submission deadlines are set annually for early February, with upcoming due dates on February 5, 2025, and February 5, 2026. Contact information includes several NSF program directors across participating directorates. For instance, inquiries may be directed to Stacey Levine (slevine@nsf.gov, 703-292-2948) and others listed in the solicitation. Applicants are encouraged to explore the NSF website for updates, proposal guidelines, and further resources to assist in preparing competitive applications.