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 787 117

  2. ReProver ReProver Public

    Retrieval-Augmented Theorem Provers for Lean

    Python 321 69

  3. LeanCopilot LeanCopilot Public

    LLMs as Copilots for Theorem Proving in Lean

    C++ 1.3k 123

Repositories

Showing 10 of 11 repositories
  • 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 60 Apache-2.0 11 2 1 Updated Mar 10, 2026
  • LeanDojoWebsite Public

    Code for LeanDojo's website

    lean-dojo/LeanDojoWebsite’s past year of commit activity
    HTML 8 MIT 3 0 0 Updated Feb 28, 2026
  • LeanCopilot Public

    LLMs as Copilots for Theorem Proving in Lean

    lean-dojo/LeanCopilot’s past year of commit activity
    C++ 1,256 MIT 123 4 0 Updated Feb 17, 2026
  • lean4code Public

    Lean4 Code Editor

    lean-dojo/lean4code’s past year of commit activity
    TypeScript 15 MIT 1 0 0 Updated Jan 28, 2026
  • LeanDojo Public

    Tool for data extraction and interacting with Lean programmatically.

    lean-dojo/LeanDojo’s past year of commit activity
    Python 787 MIT 117 6 (1 issue needs help) 6 Updated Jan 18, 2026
  • LeanMillenniumPrizeProblems Public

    Formalization of the Millennium Problems in Lean 4

    lean-dojo/LeanMillenniumPrizeProblems’s past year of commit activity
    Lean 47 Apache-2.0 6 2 0 Updated Jan 16, 2026
  • LeanProgress Public

    Guiding Search for Neural Theorem Proving via Proof Progress Prediction

    lean-dojo/LeanProgress’s past year of commit activity
    Python 3 MIT 0 1 0 Updated Jan 10, 2026
  • LeanAgent Public

    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.

    lean-dojo/LeanAgent’s past year of commit activity
    Python 60 19 1 3 Updated Jun 13, 2025
  • LeanVision Public
    lean-dojo/LeanVision’s past year of commit activity
    Python 2 1 0 0 Updated Mar 11, 2025
  • ReProver Public

    Retrieval-Augmented Theorem Provers for Lean

    lean-dojo/ReProver’s past year of commit activity
    Python 321 MIT 69 1 0 Updated Jan 30, 2025
View all repositories

Most used topics

Loading…