A team of UCLA computer scientists and mathematicians has been awarded a three-year, $5 million grant by the Defense Advanced Research Projects Agency to develop artificial intelligence tools aimed at transforming how mathematical discoveries are made, formalized and verified.
The project, titled “ALPHA” — Accelerated Formal Proof Synthesis with Neuro-Symbolic Automation — is led by Wei Wang, a professor and chair of the Computer Science Department at the UCLA Samueli School of Engineering.
Other ALPHA team members include:
- Andrea Bertozzi, distinguished professor of mathematics and mechanical and aerospace engineering and holder of UCLA’s Betsy Wood Knapp Chair for Innovation and Creativity
- Kai-Wei Chang, associate professor of computer science
- Nanyun (Violet) Peng, associate professor of computer science
- Amit Sahai, a professor of computer science and mathematics and holder of the Symantec Term Chair in Computer Science
- Terence Tao, professor of mathematics, holder of the James and Carol Collins Chair and director of special projects at the Institute for Pure and Applied Mathematics
Progress in mathematics remains relatively slow compared with other fields for two primary reasons. First, breaking down complex problems into smaller components, known as lemmas, is a time-intensive manual process. Second, proving those lemmas requires significant effort and expertise.
To address these challenges, ALPHA will automate key aspects of mathematical reasoning, including theorem decomposition, lemma identification and the generation of novel proof strategies. The open-source AI platform will also translate seamlessly between natural language and formal proof systems while maintaining precision.
The project will focus on three major areas of mathematics — partial differential equations, number theory and complexity theory — with the goal of solving advanced mathematical problems and extending its impact beyond these core areas.
By integrating open-source proof assistants such as Lean and Isabelle, ALPHA will ensure output accuracy while leveraging existing formal libraries and developer communities. Built upon advances in large language models, neuro-symbolic AI, code generation and automated theorem proving, the system aims to bridge human intuition and machine verification to fundamentally reshape mathematical research.
“This is a major step toward bridging human intuition and machine verification,” said Wang, who holds the Leonard Kleinrock Term Chair in Computer Science. “Our goal is to fundamentally expand how mathematicians explore and validate new ideas.”
UCLA is one of 13 university-based teams selected March 21 for DARPA’s expMATH (Exponentiating Mathematics) program. The initiative seeks to accelerate progress in pure mathematics by developing AI systems that can function as collaborative research partners.