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

No results found

Latest Lean Stable:

leanprover/lean4:v4.28.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 815dd04 builds on the recent leanprover/lean4:v4.29.0-rc6
    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 4c0618b fails to build on leanprover/lean4:v4.29.0-rc6
    ryu
    Converts floating point numbers to decimal strings
  4. Commit bbecd66 builds on the recent leanprover/lean4:v4.29.0-rc6 after lake update
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  5. Commit fd086a7 builds on the old leanprover/lean4:v4.27.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  6. Commit 002a19b builds on the recent leanprover/lean4:v4.28.0
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit c1cdc44 builds on the recent leanprover/lean4:v4.28.0
    PhysLean
    A project to digitalise results from physics into Lean.
  8. Commit fea2a7c builds on the recent leanprover/lean4:v4.29.0-rc6 after lake update
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  9. Commit 4de9edc 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 2bf0e10 builds on the old leanprover/lean4:v4.21.0
    mil
    The user home repository for the Mathematics in Lean tutorial.
All most popular

Newly Created

  1. Commit ebae19e builds on the recent leanprover/lean4:v4.28.0
    NormalForms
    Executable Hermite and Smith Normal Forms in Lean 4 over Euclidean Domains, with a PID bridge to mathlib.
  2. Commit 5088a7b builds on the recent leanprover/lean4:v4.29.0-rc6
    LiterateLean
    literate programming for lean4
  3. Commit 6886b91 builds on the recent leanprover/lean4:v4.28.0
    shannon-entropy
    A formalization of Shannon's seminal 1948 paper defining entropy.
  4. Commit 1c76bd3 builds on the recent leanprover/lean4:v4.29.0-rc6
    lambdasat-lean
    Formally verified equality saturation engine in Lean 4, parameterized by typeclasses. OptiSat provides a domain-agnostic e-graph with 248 theorems
  5. Commit 9d2cff4 builds on the recent leanprover/lean4:v4.28.0
    sensitivity
    Lean 4 formalization of the Sensitivity Conjecture (Huang 2019)
  6. Commit 9dfee1c builds on the recent leanprover/lean4:v4.28.0
    LeanServer
    Verified HTTPS server in Lean 4 — TLS 1.3, HTTP/2, QUIC, WebSocket, gRPC — 914 machine-checked theorems, zero sorry. Pure library available (LeanServerPure).
  7. Commit aa04b54 builds on the recent leanprover/lean4:v4.28.0
    Distributed2Coloring
    2-Coloring Cycles in One Round: Formalization in Lean 4
  8. Commit 9a61202 builds on the old leanprover/lean4:v4.24.0
    Velvet
    An auto-active verifier embedded into Lean
  9. Commit 24c8d36 builds on the recent leanprover/lean4:v4.29.0-rc6 after lake update
    amo-lean
    Verified Optimizing Compiler for Cryptographic Primitives
  10. Commit c3d7547 builds on the recent leanprover/lean4:v4.28.0-rc1
    OSforGFF
    A Lean 4 formalization of the Gaussian Free Field in d=4 and proof of the Osterwalder-Schrader axioms
All newly created

Recently Updated

  1. Commit 815dd04 builds on the recent leanprover/lean4:v4.29.0-rc6
    mathlib
    The math library of Lean 4
  2. Commit 8598cb4 builds on the old leanprover/lean4:v4.8.0-rc1 after lake update
    printiest
    A pretty printer for Lean 4
  3. Commit c3d7547 builds on the recent leanprover/lean4:v4.28.0-rc1
    OSforGFF
    A Lean 4 formalization of the Gaussian Free Field in d=4 and proof of the Osterwalder-Schrader axioms
  4. Commit c336170 builds on the recent leanprover/lean4:v4.29.0-rc6
    aesop
    White-box automation for Lean 4
  5. Commit e757ea2 builds on the recent leanprover/lean4:v4.28.0
    PrimeNumberTheoremAnd
    Blueprint for the PNT+ Project
  6. Commit 3a5bc7a builds on the old leanprover/lean4:v4.25.2
    sgc
    Lean 4 library characterizing the algebraic structure of metastability and consolidation in stochastic systems
  7. Commit ab68a1a builds on the recent leanprover/lean4:v4.29.0-rc6
    VD
    Formalizing Value Distribution Theory
  8. Commit ec9f423 builds on the recent leanprover/lean4:v4.28.0
    BrownianMotion
    Construction of a Brownian Motion in Lean
  9. Commit f63184a builds on the old leanprover/lean4:v4.26.0
    leanaide
    Tools based on AI for helping with Lean 4
  10. Commit 02509f4 builds on the old leanprover/lean4:v4.25.2
    Curve25519Dalek
    Verifying curve25519-dalek using Lean
All recently updated