Skip to content
@lean-dojo

LeanDojo

Machine Learning for Theorem Proving in Lean

Pinned Loading

  1. LeanDojo LeanDojo Public

    Tool for data extraction and interacting with Lean programmatically.

    Python 841 119

  2. ReProver ReProver Public

    Retrieval-Augmented Theorem Provers for Lean

    Python 338 73

  3. LeanCopilot LeanCopilot Public

    LLMs as Copilots for Theorem Proving in Lean

    C++ 1.3k 128

Repositories

Showing 10 of 17 repositories
  • LeanCopilot Public

    LLMs as Copilots for Theorem Proving in Lean

    lean-dojo/LeanCopilot's past year of commit activity
    C++ 1,328 MIT 128 0 0 Updated Oct 1, 2026
  • LeanProfiler Public

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

    lean-dojo/LeanProfiler's past year of commit activity
    Lean 4 MIT 1 0 0 Updated Sep 30, 2026
  • FloatLib Public

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

    lean-dojo/FloatLib's past year of commit activity
    SMT 59 MIT 6 1 0 Updated Sep 30, 2026
  • TorchLean Public

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

    lean-dojo/TorchLean's past year of commit activity
    Lean 165 MIT 20 0 5 Updated Sep 30, 2026
  • Euler Public

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

    lean-dojo/Euler's past year of commit activity
    Lean 0 Apache-2.0 0 0 0 Updated Sep 23, 2026
  • LeanDojoWebsite Public

    Code for LeanDojo's website

    lean-dojo/LeanDojoWebsite's past year of commit activity
    HTML 8 MIT 3 0 0 Updated Sep 18, 2026
  • LeanMillenniumPrizeProblems Public

    Formalization of the Millennium Problems in Lean 4

    lean-dojo/LeanMillenniumPrizeProblems's past year of commit activity
    Lean 68 Apache-2.0 17 0 0 Updated Sep 14, 2026
  • lean4code Public

    Lean4 Code Editor

    lean-dojo/lean4code's past year of commit activity
    TypeScript 19 MIT 3 1 0 Updated Aug 18, 2026
  • LeanDojo-v2 Public

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

    lean-dojo/LeanDojo-v2's past year of commit activity
    Python 141 Apache-2.0 22 1 1 Updated Aug 10, 2026
  • ITPEval Public

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

    lean-dojo/ITPEval's past year of commit activity
    Standard ML 3 MIT 0 0 0 Updated Jul 8, 2026
View all repositories