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 a535bdc builds on the recent leanprover/lean4:v4.30.0-rc2
    mathlib
    The math library of Lean 4
  2. Commit 4f623b0 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 e08558f builds on the old leanprover/lean4:v4.27.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  6. Commit 31d4149 builds on the recent leanprover/lean4:v4.30.0-rc2
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit ca9680e builds on the old leanprover/lean4:v4.29.0
    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 d69afe6 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 b88523b 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 45f66bf 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 7f8b132 builds on the recent leanprover/lean4:v4.30.0-rc2 after lake update
    EvmAsm
  2. Commit b6170b7 builds on the old leanprover/lean4:v4.28.0
    Strata
  3. Commit 0a7cc0d builds on the old leanprover/lean4:v4.29.0 after lake update
    SpherePacking
    A Lean formalisation of Maryna Viazovska's Fields Medal-winning solution to the sphere packing problem in dimension 8.
  4. Commit 24c8d36 builds on the old leanprover/lean4:v4.29.0-rc6 after lake update
    amo-lean
    Verified Optimizing Compiler for Cryptographic Primitives
  5. Commit 1ae7958 builds on the recent leanprover/lean4:v4.30.0-rc2
    Parser
    Parser Combinator Library for Lean 4
  6. Commit 1942a83 builds on the old leanprover/lean4:v4.29.0-rc1
    proetale
    Proétale cohomology in Lean
  7. Commit a535bdc builds on the recent leanprover/lean4:v4.30.0-rc2
    mathlib
    The math library of Lean 4
  8. Commit 978ec8a builds on the old leanprover/lean4:v4.29.0
    iris
    Lean 4 port of Iris, a higher-order concurrent separation logic framework
  9. Commit bc67776 builds on the recent leanprover/lean4:v4.30.0-rc2
    soma-workspace
    ⚗️ | Soma is a general-purpose dependently-typed functional programming language powered by Interaction Nets with a minimal runtime.
  10. Commit d69afe6 builds on the old leanprover/lean4:v4.20.1
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
All recently updated