The Artificial Intelligence, Formal Methods, and Mathematical Reasoning (AIMing) program supports research at the interface of innovative computational and artificial intelligence (AI) technologies and new strategies/technologies in mathematical reasoning to automate knowledge discovery. The program seeks to advance machine-assisted mathematical reasoning, encompassing conjecture, proof, and verification, and has the potential to impact research in AI. Key aspects of this opportunity include: • The program is focused on the intersection of AI, formal methods, and mathematical reasoning. • Eligible applicants include non-profit, non-academic organizations and institutions of higher education. • The estimated funding for this program is 6,000,000, with an award ceiling of 1,200,000. • The program aims to support research that can automate knowledge discovery and has the potential to impact AI research.