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

No results found

Latest Lean Stable:

leanprover/lean4:v4.32.2
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 9359494 builds on the recent leanprover/lean4:v4.33.0-rc1
    mathlib
    The math library of Lean 4
  2. Commit 0fa0212 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.33.0-rc1
    ryu
    Converts floating point numbers to decimal strings
  4. Commit 2458f73 builds on the recent leanprover/lean4:v4.33.0-rc1 after lake update
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  5. Commit fadb320 builds on the old leanprover/lean4:v4.27.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  6. Commit 32450dd builds on the recent leanprover/lean4:v4.33.0-rc1
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit 17315ee builds on the recent leanprover/lean4:v4.32.0
    Physlib
    A project to digitalise results from physics into Lean.
  8. Commit 3491c62 builds on the recent leanprover/lean4:v4.33.0-rc1
    cslib
    The Lean Computer Science Library (CSLib)
  9. Commit dd6d752 builds on the old leanprover/lean4:v4.30.0
    mil
    The user home repository for the Mathematics in Lean tutorial.
  10. Commit 7e276a2 builds on the old leanprover/lean4:v4.29.1
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
All most popular

Newly Created

  1. Commit a4ca5ad fails to build on leanprover/lean4:v4.32.1
    Calculus_21
    An Universe for Mitar —— Classical Calculus
  2. Commit f8a851a builds on the recent leanprover/lean4:v4.32.2
    proofnet-ir
    Verified proof-geometry IR experiments for AI-guided theorem proving in Lean 4
  3. Commit a2fc5bd fails to build on leanprover/lean4:v4.32.1
    ProbabilityApproximation
    Lean 4 and Mathlib formalization of nonuniform Berry–Esseen bounds and Bentkus's multivariate Gaussian approximation over convex sets.
  4. Commit 8f2ee54 builds on the recent leanprover/lean4:v4.32.0
    pacioli
    A verified core of accounting mechanics in Lean 4, paired with curated accounting judgment in the Open Knowledge Format (OKF).
  5. Commit 5c667c3 builds on the recent leanprover/lean4:v4.32.2
    domain-theory
    A Lean Library for Domain Theory
  6. Commit 0291784 fails to build on leanprover/lean4:v4.32.1
    SHSLib
    Stochastic Hybrid Systems core definitions formalized in Lean
  7. Commit c196b63 fails to build on leanprover/lean4:v4.32.1
    SeibergWitten
    The Seiberg-Witten solution of N=2 SU(2) super-Yang-Mills, formalized in Lean 4: physics as named postulates, machine-checked consequences, audited assumptions
  8. Commit 0a4ec3a builds on the recent leanprover/lean4:v4.33.0-rc1
    Quantum4Lean
    Verified quantum computing in Lean 4 with FFI bridge to Apple Silicon (Metal 3). Full NISQ stack, dependent types, formal circuit verification, and mathematical translators to Hamiltonians for autonomous AI.
  9. Commit 7998024 builds on the old leanprover/lean4:v4.31.0
    lean-linq
    Type-safe, deeply-embedded SQL query DSL for Lean 4 — LINQ-style pipelines and query! comprehensions compiling to parameterized SQL for SQLite, PostgreSQL, and SQL Server
  10. Commit fb9c583 builds on the old leanprover/lean4:v4.29.1
    SafeVerify
    Leanstral's fork of SafeVerify, which we use for code agent training and as part of our evaluation stack.
All newly created

Recently Updated

  1. Commit 1ac1ffa builds on the recent leanprover/lean4:v4.32.2
    linglib
    A Lean 4 library for formal linguistics: semantics, syntax, pragmatics, morphology, phonology, and processing — formalized across competing frameworks for high interconnection density.
  2. Commit 3975cca builds on the old leanprover/lean4:v4.31.0
    Arklib
    Formally Verified Arguments of Knowledge in Lean
  3. Commit 7c5801e builds on the recent leanprover/lean4:v4.33.0-rc1
    verso-manual
    The Lean reference manual
  4. Commit 655d4f6 builds on the recent leanprover/lean4:v4.33.0-rc1
    verso
    Lean documentation authoring tool
  5. Commit 79be81f builds on the recent leanprover/lean4:v4.33.0-rc1
    verso-slides
  6. Commit a50233d builds on the recent leanprover/lean4:v4.33.0-rc1
    PrimeCert
    Formal prime certificates in Lean 4
  7. Commit eead15f builds on the old leanprover/lean4:v4.30.0-rc2 after lake update
    EvmAsm
  8. Commit 6b0b76c builds on the recent leanprover/lean4:v4.33.0-rc1
    subverso
  9. Commit 1d23837 builds on the recent leanprover/lean4:v4.33.0-rc1
    REPL
    A simple REPL for Lean 4, returning information about errors and sorries.
  10. Commit 0fa0212 builds on the old leanprover/lean4:v4.29.0-rc8
    Analysis
    A Lean companion to Analysis I
All recently updated