AI-Driven Formal Theorem Proving

California Institute of Technology, PI: Anima Anandkumar
Code

The Grand Challenge

The challenge is to formalize and verify everything—from programs, to scientific experiments, to mathematics. Our lab is working on making verification accessible, mathematically rigorous, and practical by combining large language models with formal proof assistants like Lean. We want to bring formal methods to broader scientific computing, where correctness matters for reproducible research and trustworthy software.

Papers

Mathematical Discovery and Formalization Towards the AC Conjecture
Caroline Zhang, Aaron Zhao, Robert Joseph George, Sergei Gukov, Anima Anandkumar
NeurIPS Mathematical Reasoning and AI, 2025
NeurIPS Workshop

LeanDojo-v2: A Comprehensive Library for AI-Assisted Theorem Proving in Lean
Ryan Hsiang, Will Adkisson, Robert Joseph George, Anima Anandkumar
NeurIPS Mathematical Reasoning and AI, 2025
NeurIPS Workshop

LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction
Robert Joseph George, Suozhi Huang, Anima Anandkumar et al.
Transactions on Machine Learning Research (TMLR), 2025
arXiv:2502.17925

LeanAgent: Lifelong Learning for Formal Theorem Proving
Adarsh Kumarappan, Mo Tiwari, Peiyang Song, Robert Joseph George, Chaowei Xiao, Anima Anandkumar
International Conference on Learning Representations (ICLR) 2025
arXiv:2410.06209

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
Peiyang Song, Kaiyu Yang, Anima Anandkumar
International Conference on Neuro-symbolic Systems (NeuS) 2025
arXiv:2404.12534

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, Anima Anandkumar
Neural Information Processing Systems (NeurIPS) 2023
arXiv:2306.15626