LeanDojo

Lean proofs for the derivations in Singularity of the Euler Equations on R^3

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

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

Arbitrary verified fast precision floating point arithmetic in Lean, with proofs, optimized backends, and support for IEEE binary and decimal, posits, and custom formats.

LLMs as Copilots for Theorem Proving in Lean

Code for LeanDojo's website

Formalization of the Millennium Problems in Lean 4

Lean4 Code Editor

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

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