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 72b9c8d builds on the recent leanprover/lean4:v4.29.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 4c0618b fails to build on leanprover/lean4:v4.29.0-rc2
    ryu
    Converts floating point numbers to decimal strings
  4. Commit bbecd66 builds on the recent leanprover/lean4:v4.29.0-rc2 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 a48ce3f builds on the recent leanprover/lean4:v4.28.0
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit 6286c6b 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-rc2 after lake update
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  9. Commit 9d809ba 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 12b17c2 fails to build on leanprover/lean4:v4.29.0-rc2
    lib
    A formalization of Shannon's seminal 1948 paper defining entropy.
  2. Commit 0a16de9 fails to build on leanprover/lean4:v4.29.0-rc2
    sensitivity
    Lean 4 formalization of the Sensitivity Conjecture (Huang 2019)
  3. Commit 9dfee1c fails to build on leanprover/lean4:v4.29.0-rc2
    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).
  4. Commit 9a61202 builds on the old leanprover/lean4:v4.24.0
    Velvet
    An auto-active verifier embedded into Lean
  5. Commit 24c8d36 builds on the recent leanprover/lean4:v4.29.0-rc2 after lake update
    amo-lean
    Verified Optimizing Compiler for Cryptographic Primitives
  6. 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
  7. Commit 4aa3287 builds on the recent leanprover/lean4:v4.28.0
    Coinductive
    Co-inductive datatypes for Lean
  8. Commit 6e27c1b builds on the old leanprover/lean4:v4.26.0
    PartialRegularity
    Lean formalizations for the paper "Almost all primes are partially regular"
  9. Commit 3b00bde builds on the old leanprover/lean4:v4.26.0
    Deadends
  10. Commit e1f334f builds on the recent leanprover/lean4:v4.29.0-rc2
    tvm-lean
All newly created

Recently Updated

  1. Commit 75956ee builds on the recent leanprover/lean4:v4.28.0-rc1
    BrownianMotion
    Construction of a Brownian Motion in Lean
  2. Commit 6286c6b builds on the recent leanprover/lean4:v4.28.0
    PhysLean
    A project to digitalise results from physics into Lean.
  3. Commit c6684d6 builds on the recent leanprover/lean4:v4.28.0
    PrimeNumberTheoremAnd
    Blueprint for the PNT+ Project
  4. Commit 3d91ad1 builds on the old leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  5. Commit 72b9c8d builds on the recent leanprover/lean4:v4.29.0-rc2
    mathlib
    The math library of Lean 4
  6. Commit d12e71b builds on the recent leanprover/lean4:v4.28.0
    Noperthedron
    The Noperthedron does not have Rupert Property: a proof in Lean4
  7. Commit b42031a builds on the recent leanprover/lean4:v4.28.0
    Arklib
    Formally Verified Arguments of Knowledge in Lean
  8. Commit 8ad46d9 builds on the recent leanprover/lean4:v4.29.0-rc2
    tryAtEachStep
    Try a tactic at each step in a Lean proof.
  9. Commit a381813 builds on the recent leanprover/lean4:v4.29.0-rc2 after lake update
    reap
    General neural tactic for Lean 4
  10. Commit 824fd94 builds on the recent leanprover/lean4:v4.29.0-rc2
    Heights
    An attempt at formalizing the theory of heights in Lean
All recently updated