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

No results found

Latest Lean Stable:

leanprover/lean4:v4.29.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
    ryu
    Converts floating point numbers to decimal strings
  4. Commit bbecd66 builds on the recent leanprover/lean4:v4.29.0 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 old leanprover/lean4:v4.28.0
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit e5eaf63 builds on the old 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 efaa113 builds on the old leanprover/lean4:v4.28.0
    FormalQualBench
  2. Commit 794097f fails to build on leanprover/lean4:v4.29.0
    leslie
  3. Commit 4286173 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.
  4. Commit 5088a7b builds on the recent leanprover/lean4:v4.29.0
    LiterateLean
    literate programming for lean4
  5. Commit bc71711 fails to build on leanprover/lean4:v4.29.0
    Cookbook
    A cookbook for Metaprogramming in Lean4 containing code snippets to help you code!
  6. Commit 6886b91 builds on the old leanprover/lean4:v4.28.0
    shannon-entropy
    A formalization of Shannon's seminal 1948 paper defining entropy.
  7. Commit 0439a64 builds on the recent leanprover/lean4:v4.29.0
    optisat
    Formally verified equality saturation engine in Lean 4, parameterized by typeclasses. OptiSat provides a domain-agnostic e-graph with 248 theorems
  8. Commit 9d2cff4 builds on the old leanprover/lean4:v4.28.0
    sensitivity
    Lean 4 formalization of the Sensitivity Conjecture (Huang 2019)
  9. Commit 9dfee1c builds on the old 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).
  10. Commit aa04b54 builds on the old leanprover/lean4:v4.28.0
    Distributed2Coloring
    2-Coloring Cycles in One Round: Formalization in Lean 4
All newly created

Recently Updated

  1. Commit 011fe96 builds on the old leanprover/lean4:v4.28.0
    Gossip
    Verified Results about Gossip protocols in Lean 4
  2. Commit e7f4c8d builds on the old leanprover/lean4:v4.28.0
    VCVio
    Formalized Cryptography Proofs in Lean 4
  3. Commit 6f1214c builds on the old leanprover/lean4:v4.25.2
    Clean
    Lean circuit DSL
  4. Commit 45f0097 builds on the old leanprover/lean4:v4.28.0
    Arklib
    Formally Verified Arguments of Knowledge in Lean
  5. Commit 8c5b27c builds on the old leanprover/lean4:v4.28.0-rc1
    Foundation
    Formalization of Mathematical Logic
  6. Commit be4ae49 builds on the recent leanprover/lean4:v4.29.0
    verso
    Lean documentation authoring tool
  7. Commit d928197 builds on the recent leanprover/lean4:v4.29.0
    soma-workspace
    ⚗️ | Soma is a general-purpose dependently-typed functional programming language powered by Interaction Nets with a minimal runtime.
  8. Commit a381813 builds on the recent leanprover/lean4:v4.29.0-rc6 after lake update
    reap
    General neural tactic for Lean 4
  9. Commit 815dd04 builds on the recent leanprover/lean4:v4.29.0-rc6
    mathlib
    The math library of Lean 4
  10. Commit 7d99667 builds on the old leanprover/lean4:v4.27.0
    glimpseOfLean
    An introduction to theorem proving in Lean for the impatient.
All recently updated