LeanDojo ORG

Tool for data extraction and interacting with Lean programmatically.

Retrieval-Augmented Theorem Provers for Lean

LLMs as Copilots for Theorem Proving in Lean

ChatGPT plugin for theorem proving in Lean

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

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

LeanAgent is a novel lifelong learning framework for formal theorem proving that continuously generalizes to and improves on ever-expanding mathematical knowledge without forgetting previously learned knowledge.

Formalization of the Millennium Problems in Lean 4

Lean4 Code Editor

Code for LeanDojo's website

Guiding Search for Neural Theorem Proving via Proof Progress Prediction

No description.

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

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

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