Repositories list

• lean4code

  Public
  Lean4 Code Editor

  TypeScript

  •

  MIT License

  •1•13•0•0•Updated Jan 28, 2026Jan 28, 2026

• LeanDojoWebsite

  Public
  Code for LeanDojo's website

  machine-learningtheorem-provinglean+ 2lean4llm

  JavaScript

  •

  MIT License

  •3•8•0•0•Updated Jan 23, 2026Jan 23, 2026

• LeanDojo

  Public
  Tool for data extraction and interacting with Lean programmatically.

  machine-learningtheorem-provinglean+ 2lean4llm

  Python

  •

  MIT License

  •117•762•6•6•Updated Jan 18, 2026Jan 18, 2026

• LeanMillenniumPrizeProblems

  Public

  lean-dojo/LeanMillenniumPrizeProblems’s past year of commit activity
  Formalization of the Millennium Problems in Lean 4

  mathematicsformalizationmillennium-problems+ 1lean4

  Lean

  •

  Apache License 2.0

  •5•41•2•0•Updated Jan 16, 2026Jan 16, 2026

• LeanProgress

  Public
  Guiding Search for Neural Theorem Proving via Proof Progress Prediction

  machine-learningtheorem-provingrl+ 6leanformal-mathematicsproof-searchlean4llmprogress-prediction

  Python

  •

  MIT License

  •0•3•1•0•Updated Jan 10, 2026Jan 10, 2026

• LeanCopilot

  Public

  lean-dojo/LeanCopilot’s past year of commit activity
  LLMs as Copilots for Theorem Proving in Lean

  machine-learningtheorem-provinglean+ 4formal-mathematicslean4llmllm-inference

  C++

  •

  MIT License

  •122•1.2k•4•0•Updated Jan 10, 2026Jan 10, 2026

• LeanDojo-v2

  Public

  lean-dojo/LeanDojo-v2’s past year of commit activity
  LeanDojo-v2 is an end-to-end framework for training, evaluating, and deploying AI-assisted theorem provers for Lean 4.

  machine-learninglibrarytheorem-proving+ 1lean4

  Python

  •

  Apache License 2.0

  •2•18•1•0•Updated Dec 31, 2025Dec 31, 2025

• LeanAgent

  Public

  lean-dojo/LeanAgent’s past year of commit activity
  LeanAgent is a novel lifelong learning framework for formal theorem proving that continuously generalizes to and improves on ever-expanding mathematical knowled…

  agentcontinual-learninglean4

  Python

  •17•53•1•3•Updated Jun 13, 2025Jun 13, 2025

• LeanVision

  Public

  lean-dojo/LeanVision’s past year of commit activity
  Python

  •1•1•0•0•Updated Mar 11, 2025Mar 11, 2025

• ReProver

  Public
  Retrieval-Augmented Theorem Provers for Lean

  machine-learningtheorem-provinglean+ 2lean4llm

  Python

  •

  MIT License

  •69•317•1•0•Updated Jan 30, 2025Jan 30, 2025

• LeanDojoChatGPT

  Public

  lean-dojo/LeanDojoChatGPT’s past year of commit activity
  ChatGPT plugin for theorem proving in Lean

  machine-learningtheorem-provinglean+ 4lean4large-language-modelschatgptchatgpt-plugin

  Python

  •

  MIT License

  •15•124•1•0•Updated Apr 4, 2024Apr 4, 2024