ALPHA stands for Accelerated Formal Proof Synthesis with Neuro-Symbolic Automation and is led by Wei Wang, professor and chair of UCLA's Computer Science Department.

The project seeks to automate core mathematical reasoning tasks, including decomposing theorems into lemmas, identifying lemmas, and generating novel proof strategies.

ALPHA will translate between natural language and formal proof languages, preserve precision, and rely on open-source proof assistants like Lean and Isabelle to ensure output accuracy.

ALPHA will leverage established formal libraries and developer communities by integrating tools like Lean and Isabelle, operating within the expMATH program to accelerate progress in pure mathematics.

Key members span computer science and mathematics, including Andrea Bertozzi, Kai-Wei Chang, Nanyun (Violet) Peng, Amit Sahai, and Terence Tao.

The initiative builds on advances in large language models, neuro-symbolic AI, code generation, and automated theorem proving to bridge human intuition with machine-verified results.

The work targets partial differential equations, number theory, and complexity theory, aiming to tackle advanced problems and broaden impact beyond these domains.

UCLA researchers secured a three-year, $5 million DARPA grant to develop ALPHA, an AI system designed to accelerate mathematical discovery, formalization, and verification.