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

No results found

Latest Lean Stable:

leanprover/lean4:v4.30.0-rc2
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 028964f builds on the recent leanprover/lean4:v4.30.0-rc2
    mathlib
    The math library of Lean 4
  2. Commit 801fd1b builds on the old leanprover/lean4:v4.29.0-rc8
    Analysis
    A Lean companion to Analysis I
  3. Commit 4c0618b fails to build on leanprover/lean4:v4.30.0-rc2
    ryu
    Converts floating point numbers to decimal strings
  4. Commit bbecd66 builds on the recent leanprover/lean4:v4.30.0-rc2 after lake update
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  5. Commit 880c27e builds on the old leanprover/lean4:v4.27.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  6. Commit 1f76653 builds on the recent leanprover/lean4:v4.30.0-rc2
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit c1b3fb8 builds on the recent leanprover/lean4:v4.29.1
    Physlib
    A project to digitalise results from physics into Lean.
  8. Commit c944afd builds on the old leanprover/lean4:v4.29.0-rc8
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  9. Commit b99c0e4 builds on the old leanprover/lean4:v4.20.1
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  10. Commit 870e11e builds on the recent leanprover/lean4:v4.30.0-rc2
    cslib
    The Lean Computer Science Library (CSLib)
All most popular

Newly Created

  1. Commit 4305eae builds on the old leanprover/lean4:v4.28.0
    langlib
    Library for formal language theory in Lean 4
  2. Commit efaa113 builds on the old leanprover/lean4:v4.28.0
    FormalQualBench
  3. Commit 74f0266 builds on the old leanprover/lean4:v4.29.0
    Algolean
    Algorithms and Complexity Library using the lightweight query combinator framework called "Prog"
  4. Commit 9abf4dc builds on the old leanprover/lean4:v4.27.0
    leslie
  5. Commit e90c69c builds on the old leanprover/lean4:v4.28.0
    NormalForms
    Executable Hermite and Smith Normal Forms in Lean 4 over Euclidean Domains, with a PID bridge to mathlib.
  6. Commit 5088a7b builds on the recent leanprover/lean4:v4.30.0-rc2
    LiterateLean
    literate programming for lean4
  7. Commit 18c12de builds on the old leanprover/lean4:v4.28.0
    Cookbook
    A cookbook for Metaprogramming in Lean4 containing code snippets to help you code!
  8. Commit 6886b91 builds on the old leanprover/lean4:v4.28.0
    shannon-entropy
    A formalization of Shannon's seminal 1948 paper defining entropy.
  9. Commit 0439a64 builds on the recent leanprover/lean4:v4.30.0-rc2
    optisat
    Formally verified equality saturation engine in Lean 4, parameterized by typeclasses. OptiSat provides a domain-agnostic e-graph with 248 theorems
  10. Commit 9d2cff4 builds on the old leanprover/lean4:v4.28.0
    sensitivity
    Lean 4 formalization of the Sensitivity Conjecture (Huang 2019)
All newly created

Recently Updated

  1. Commit 2840112 builds on the old leanprover/lean4:v4.28.0
    sal
    Implementation of Neem using Lean
  2. Commit 71f840a builds on the recent leanprover/lean4:v4.29.1
    Strata
  3. Commit 55e48a2 builds on the old leanprover/lean4:v4.28.0
    Clean
    Lean circuit DSL
  4. Commit 5169c93 builds on the recent leanprover/lean4:v4.30.0-rc2
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  5. Commit 028964f builds on the recent leanprover/lean4:v4.30.0-rc2
    mathlib
    The math library of Lean 4
  6. Commit 7f8b132 builds on the recent leanprover/lean4:v4.30.0-rc2 after lake update
    EvmAsm
  7. Commit a6047b2 builds on the old leanprover/lean4:v4.28.0
    pdl
    Tableaux for Propositional Dynamic Logic in Lean 4 (WORK IN PROGRESS)
  8. Commit 870e11e builds on the recent leanprover/lean4:v4.30.0-rc2
    cslib
    The Lean Computer Science Library (CSLib)
  9. Commit ab5be92 builds on the recent leanprover/lean4:v4.30.0-rc2
    verso-manual
    The Lean reference manual
  10. Commit 24fe0a1 builds on the old leanprover/lean4:v4.29.0
    ix
    a zero-knowledge proof-carrying code platform for Lean 4
All recently updated