AI-Driven Formal Theorem Proving

California Institute of Technology, PI: Anima Anandkumar, Grad Student: Robert Joseph George
Code

The Grand Challenge

We care about a future where important scientific and mathematical work can be checked, trusted, and built on with confidence. Our lab develops tools that make formal verification more approachable and useful in practice, using large language models together with proof assistants like Lean. Our interests span scientific computing, software, experimental workflows, and pure mathematics: anywhere correctness, reproducibility, and rigorous reasoning matter.

We also believe this work should be open and collaborative. Our tools, benchmarks, datasets, and research artifacts are open sourced whenever possible, so that others can inspect them, build on them, and help improve them. Formal verification has the potential to become part of everyday scientific practice, but that will only happen if the community can experiment with the technology, understand how it works, and adapt it to real problems across disciplines.

If this vision resonates with you, we would love to hear from you. Whether you have questions, ideas, use cases, or features you wish existed, please reach out.

Papers

TorchLean: Formalizing Neural Networks in Lean
Robert Joseph George, Jennifer Cruden, Will Adkisson, Xiangru Zhong, Huan Zhang, Anima Anandkumar
arXiv preprint, 2026
arXiv:2602.22631 ยท Code

BRIDGE: Building Representations in Domain-Guided Verified Program Synthesis
Robert Joseph George, Carson Eisenach, Udaya Ghai, Dominique Perrault-Joncas, Anima Anandkumar, Dean Foster
arXiv preprint, 2026
arXiv:2511.21104

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