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 845 121

  2. ReProver ReProver Public

    Retrieval-Augmented Theorem Provers for Lean

    Python 339 74

  3. LeanCopilot LeanCopilot Public

    LLMs as Copilots for Theorem Proving in Lean

    C++ 1.3k 130

Repositories

Showing 10 of 17 repositories
  • 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 Oct 14, 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 173 MIT 22 0 4 Updated Oct 14, 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 69 MIT 6 0 0 Updated Oct 13, 2026
  • LeanCopilot Public

    LLMs as Copilots for Theorem Proving in Lean

    lean-dojo/LeanCopilot's past year of commit activity
    C++ 1,333 MIT 130 0 0 Updated Oct 13, 2026
  • lean4code Public

    Lean4 Code Editor

    lean-dojo/lean4code's past year of commit activity
    TypeScript 19 MIT 3 1 0 Updated Oct 9, 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 70 Apache-2.0 20 1 0 Updated Sep 14, 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 146 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 4 MIT 0 0 0 Updated Jul 8, 2026
View all repositories