The first unified benchmark for quantum-science reasoning across informal natural-language solutions and Lean-oriented formal representations.

LLMs as Copilots for Theorem Proving in Lean

TorchLean is the first unified Lean 4 framework for neural-network specification, execution, and verification.

Code for LeanDojo's website

Formalization of the Millennium Problems in Lean 4

BRIDGE is a framework for program verification and synthesis in Lean.

LeanDojo-v2 is an end-to-end framework for training, evaluating, and deploying AI-assisted theorem provers for Lean 4.

Lean4 Code Editor

Tool for data extraction and interacting with Lean programmatically.

Guiding Search for Neural Theorem Proving via Proof Progress Prediction