LeanDojo

Formalization of the Millennium Problems in Lean 4

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

LLMs as Copilots for Theorem Proving in Lean

Lean4 Code Editor

Structured runtime profiling for Lean4 code, with nested spans, Perfetto traces, regression checks, and optional TorchLean integration.

LeanDojo-v2 is an end-to-end framework for training, evaluating, and deploying AI-assisted theorem provers for 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.