AI-Driven Formal Theorem Proving

Code Docs Models Dataset (Lean 3) Dataset (Lean 4)

The Grand Challenge

The integration of artificial intelligence with formal mathematics presents a critical research challenge in bridging two fundamentally different computational paradigms. Large Language Models demonstrate remarkable capabilities in mathematical reasoning and proof generation, yet suffer from inconsistencies and hallucinations that compromise logical reliability. Formal proof assistants such as Lean provide absolute verification through mechanized type theory, ensuring every mathematical statement is rigorously validated by a trusted kernel. Our central ambition is to combine the power of LLMs with Lean to produce more verifiable mathematics, code, and scientific reasoning for a wide range of downstream applications.

Our Research Program

Our laboratory has developed several different research projects that systematically explores different facets of AI-assisted theorem proving. This work is primarily driven by researchers at Caltech, under the leadership of Professor Anima Anandkumar.

Our Five Major Contributions

LeanDojo

The foundational infrastructure that bridges Python-based ML and the Lean prover, enabling data extraction and interactive environments for AI research. This work provides the essential tooling that makes all subsequent research possible.

LeanAgent

A lifelong learning framework for autonomous theorem proving that continuously improves across expanding mathematical domains without catastrophic forgetting. This represents our exploration of fully autonomous mathematical reasoning.

LeanCopilot

A human-in-the-loop assistant that seamlessly integrates LLMs into the Lean environment, providing real-time suggestions and proof automation. This work demonstrates effective human-AI collaboration in formal mathematics.

LeanProgress

A specialized system that provides global progress estimation for proof search, improving the efficiency of automated theorem proving through intelligent search guidance.

LeanIDE

An integrated development environment specifically designed for Lean theorem proving, combining modern IDE features with AI-powered assistance to create the ultimate platform for formal mathematics.