The University of California, Los Angeles (UCLA) has been awarded a $5 million grant from the Defense Advanced Research Projects Agency (DARPA) to develop an innovative AI project called ALPHA (Accelerated Formal Proof Synthesis with Neuro-Symbolic Automation). Led by Wei Wang, a professor and chair of the Computer Science Department, the project aims to automate key aspects of mathematical reasoning, including theorem decomposition and lemma identification, which are traditionally time-consuming processes. By focusing on areas such as partial differential equations, number theory, and complexity theory, ALPHA seeks to enhance the discovery and verification of advanced mathematical concepts. The open-source AI platform will facilitate seamless translation between natural language and formal proof systems, ensuring precision and accuracy. This initiative is part of DARPA's expMATH program, which aims to accelerate progress in pure mathematics by creating AI systems that can serve as collaborative research partners. Wang emphasized the project's potential to bridge human intuition with machine verification, fundamentally reshaping how mathematicians explore and validate new ideas.