UCLA Receives $5 Million DARPA Grant to Build AI for Mathematical Proof
UCLA computer scientists and mathematicians have won a three-year, $5 million grant from the Defense Advanced Research Projects Agency to develop AI tools that automate mathematical discovery and proof verification.
The project, called ALPHA (Accelerated Formal Proof Synthesis with Neuro-Symbolic Automation), is led by Wei Wang, chair of UCLA's Computer Science Department. The team includes five other faculty members: Andrea Bertozzi, Kai-Wei Chang, Nanyun Peng, Amit Sahai, and Terence Tao.
What the System Does
Mathematical progress moves slowly for two concrete reasons: breaking complex problems into smaller components called lemmas is manual and time-consuming, and proving those lemmas demands significant expertise.
ALPHA automates key steps in mathematical reasoning. It decomposes theorems, identifies useful lemmas, and generates novel proof strategies. The system translates between natural language and formal proof systems while maintaining accuracy.
The platform integrates open-source proof assistants like Lean and Isabelle to verify output and tap existing formal libraries. It builds on advances in generative AI and LLM, neuro-symbolic AI, code generation, and automated theorem proving.
Research Focus
ALPHA will concentrate on three mathematical domains: partial differential equations, number theory, and complexity theory. Results in these areas may extend to other fields.
Wang described the work as "a major step toward bridging human intuition and machine verification." The goal is to expand how mathematicians explore and validate new ideas.
Broader Initiative
UCLA is one of 13 university teams selected for DARPA's expMATH (Exponentiating Mathematics) program, announced in March 2026. The initiative aims to accelerate pure mathematics by developing AI systems that function as collaborative research partners.
Your membership also unlocks:
