LeanDojo

Code for LeanDojo's website

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

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

LLMs as Copilots for Theorem Proving in Lean

Formalization of the Millennium Problems in Lean 4

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.

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.