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

No results found

Latest Lean Stable:

leanprover/lean4:v4.27.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 85028a6 builds on the recent leanprover/lean4:v4.28.0-rc1
    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 334d08d fails to build on leanprover/lean4:v4.28.0-rc1
    ryu
    Converts floating point numbers to decimal strings
  4. Commit 6cd705a builds on the old leanprover/lean4:v4.26.0-rc2 after lake update
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  5. Commit f218287 builds on the old leanprover/lean4:v4.22.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  6. Commit 716a156 builds on the recent leanprover/lean4:v4.28.0-rc1
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit fea2a7c builds on the recent leanprover/lean4:v4.28.0-rc1 after lake update
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  8. 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.
  9. Commit fcf2471 builds on the old leanprover/lean4:v4.26.0
    PhysLean
    A project to digitalise results from physics into Lean.
  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 bacb72b builds on the recent leanprover/lean4:v4.28.0-rc1
    sparkle
    A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.
  2. Commit 5760d61 builds on the recent leanprover/lean4:v4.28.0-rc1
    leansqlite
    SQLite bindings for Lean
  3. Commit 5b3df42 builds on the recent leanprover/lean4:v4.27.0-rc1
    qdt
    Query-based Dependent Type Elaborator
  4. Commit 250d2a8 builds on the recent leanprover/lean4:v4.28.0-rc1
    LeanBench
  5. Commit 923bb91 builds on the old leanprover/lean4:v4.19.0
    LeanCat
    Lean4 benchmark on 1 category.
  6. Commit c177541 builds on the old leanprover/lean4:v4.24.0
    fineqs
    Lean4 formalization with Artistotle of the arXiv paper 1906.11174
  7. Commit c2d912e fails to build on leanprover/lean4:v4.28.0-rc1
    FelConjecture
    Lean formalizations for the paper "Fel's conjecture on syzigies of numerical semigroups"
  8. Commit b542606 builds on the old leanprover/lean4:v4.26.0
    LeanLangur
    Expositions and demos for Lean Prover
  9. Commit 9beebd8 builds on the old leanprover/lean4:v4.26.0
    ZeroToQED
    From Zero to QED: An informal introduction to formality with Lean 4
  10. Commit 7ac5820 builds on the recent leanprover/lean4:v4.28.0-rc1
    lapis
    ✏️ | A cutting-edge, concurrent & performant Language Server Protocol (LSP) framework for Lean 4.
All newly created

Recently Updated

  1. Commit fcf2471 builds on the old leanprover/lean4:v4.26.0
    PhysLean
    A project to digitalise results from physics into Lean.
  2. Commit b1c73b2 builds on the recent leanprover/lean4:v4.28.0-rc1
    PrimeNumberTheoremAnd
    Blueprint for the PNT+ Project
  3. Commit 7eb1e36 builds on the recent leanprover/lean4:v4.28.0-rc1
    software-foundations-lean
    📚 (WIP) Rewriting Software Foundations in Lean 4
  4. Commit f0d87b6 builds on the recent leanprover/lean4:v4.28.0-rc1
    cslib
    The Lean Computer Science Library (CSLib)
  5. Commit 4d47b39 builds on the recent leanprover/lean4:v4.27.0-rc1
    MCMC
    Formalization of Markov Chain Monte Carlo in Lean 4
  6. Commit 3d91ad1 builds on the old leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  7. Commit 0100f1a builds on the recent leanprover/lean4:v4.28.0-rc1
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  8. Commit 85028a6 builds on the recent leanprover/lean4:v4.28.0-rc1
    mathlib
    The math library of Lean 4
  9. Commit 334d08d fails to build on leanprover/lean4:v4.28.0-rc1
    ryu
    Converts floating point numbers to decimal strings
  10. Commit 66457c1 builds on the old leanprover/lean4:v4.26.0
    smt
    Tactics for discharging Lean goals into SMT solvers.
All recently updated