UCLA Receives $5 Million DARPA Grant to Build AI for Mathematical Research
UCLA computer scientists and mathematicians won a three-year, $5 million contract from the Defense Advanced Research Projects Agency to develop AI tools that automate key steps in 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 Fields medalist Terence Tao and five other faculty members across computer science and mathematics.
The Problem ALPHA Addresses
Mathematical progress moves slowly compared with other fields for two reasons. Breaking complex problems into smaller components called lemmas requires manual, time-intensive work. Proving those lemmas demands significant expertise and effort.
ALPHA will automate theorem decomposition, lemma identification, and the generation of proof strategies. The open-source platform translates between natural language and formal proof systems while maintaining accuracy.
How It Works
The system builds on advances in generative AI and large language models, neuro-symbolic AI, code generation, and automated theorem proving. It integrates existing proof assistants like Lean and Isabelle to verify output and tap into their developer communities.
The initial focus covers three areas: partial differential equations, number theory, and complexity theory. The goal is solving advanced problems in these domains and extending the approach elsewhere.
What This Means for Developers
ALPHA represents a shift in how research infrastructure works. Rather than replacing mathematicians, the system acts as a collaborative partner that handles routine decomposition and verification work.
For development teams, this signals growing demand for tools that bridge human reasoning and machine verification. The architecture-combining formal systems with neural models-reflects patterns likely to appear in other technical domains.
UCLA is one of 13 university teams selected for DARPA's expMATH (Exponentiating Mathematics) program, which launched March 21.
Your membership also unlocks:
