This is Reservoir, the registry for all Lean packages and documentation.

No results found

Latest Lean Stable:

leanprover/lean4:v4.24.0
Get Started with Lean

Reservoir indexes, builds, and tests packages within the Lean and Lake ecosystem. If you wish to see your package here, ensure that it meets the Reservoir inclusion criteria.

Most Popular

  1. Commit 26d3788 builds on the recent leanprover/lean4:v4.25.0-rc2
    mathlib
    The math library of Lean 4
  2. Commit 3d91ad1 builds on the old leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  3. Commit b0c844f builds on the recent leanprover/lean4:v4.25.0-rc2 after lake update
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  4. Commit 96f5ac1 builds on the recent leanprover/lean4:v4.25.0-rc2
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  5. Commit 4b3335d builds on the old leanprover/lean4:v4.22.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  6. Commit 5cfb76c builds on the recent leanprover/lean4:v4.25.0-rc2 after lake update
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  7. Commit cbb847d builds on the old leanprover/lean4:v4.20.1
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  8. Commit 53f112d builds on the old leanprover/lean4:v4.15.0-rc1
    scilean
    Scientific computing in Lean 4
  9. Commit 2bf0e10 builds on the old leanprover/lean4:v4.21.0
    mil
    The user home repository for the Mathematics in Lean tutorial.
  10. Commit b0cf6fa builds on the recent leanprover/lean4:v4.24.0
    PhysLean
    A project to digitalise results from physics into Lean.
All most popular

Newly Created

  1. Commit 58b0269 builds on the recent leanprover/lean4:v4.24.0
    Curve25519Dalek
    Verifying curve25519-dalek using Lean
  2. Commit e4acc26 builds on the recent leanprover/lean4:v4.24.0-rc1
    mathmatic_in_elementary_number_th
    IMO题目的形式化2个题
  3. Commit 351c9de builds on the recent leanprover/lean4:v4.25.0-rc2 after lake update
    category-theory-in-context-lean
    Lean Companion to the Category Theory in Context textbook by Emily Riehl
  4. Commit 878bf2d builds on the recent leanprover/lean4:v4.24.0-rc1
    RangeSetBlaze
  5. Commit c3b1b68 builds on the old leanprover/lean4:v4.23.0
    HigherCategoryTheory
    A formal verification project based on the work by Enric Cosme Llópez on "Higher-order categories".
  6. Commit 828fae5 builds on the old leanprover/lean4:v4.22.0
    TopSingleLayer
    Formal Verification of Top Single Layer Encoding
  7. Commit 942b49e builds on the old leanprover/lean4:v4.23.0-rc2
    plonky3-example
  8. Commit c04bf43 builds on the recent leanprover/lean4:v4.24.0
    LeanSage
    SageMath integration for Lean4
  9. Commit 2c841ef fails to build on leanprover/lean4:v4.25.0-rc2
    lean-sdl-test
  10. Commit 3582357 builds on the recent leanprover/lean4:v4.25.0-rc2
    SDL3
All newly created

Recently Updated

  1. Commit d555257 fails to build on leanprover/lean4:v4.25.0-rc2
    Strata
  2. Commit cbb847d builds on the old leanprover/lean4:v4.20.1
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  3. Commit 5ad890d builds on the recent leanprover/lean4:v4.25.0-rc2
    verso
    Lean documentation authoring tool
  4. Commit 26d3788 builds on the recent leanprover/lean4:v4.25.0-rc2
    mathlib
    The math library of Lean 4
  5. Commit 9370d89 builds on the old leanprover/lean4:v4.22.0
    Arklib
    Formally Verified Arguments of Knowledge in Lean
  6. Commit 5e3e7c1 builds on the recent leanprover/lean4:v4.24.0
    PrimeNumberTheoremAnd
    blueprint for prime number theorem and more
  7. Commit 2bf0e10 builds on the old leanprover/lean4:v4.21.0
    mil
    The user home repository for the Mathematics in Lean tutorial.
  8. Commit dd3edb3 builds on the recent leanprover/lean4:v4.25.0-rc2
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  9. Commit b0cf6fa builds on the recent leanprover/lean4:v4.24.0
    PhysLean
    A project to digitalise results from physics into Lean.
  10. Commit 8db2952 builds on the recent leanprover/lean4:v4.25.0-rc2
    ClassFieldTheory
    Github repository for the 2025 Clay Summer School on Formalizing Class Field Theory
All recently updated