LLMs as Copilots for Theorem Proving in Lean

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

Lean4 Code Editor

Formalization of the Millennium Problems in Lean 4

Code for LeanDojo's website

ITPEval is a benchmark suite and evaluation framework for formal statement and proof translation across Lean 4, Rocq, Isabelle/HOL, and HOL Light

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

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.

Tool for data extraction and interacting with Lean programmatically.