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 2598404 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 ed586c6 builds on the recent leanprover/lean4:v4.27.0
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  5. Commit 432d7da builds on the old leanprover/lean4:v4.22.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  6. Commit 63486c2 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 0f0ea1c builds on the recent leanprover/lean4:v4.27.0
    PhysLean
    A project to digitalise results from physics into Lean.
  9. Commit c407f90 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 b8a99fd fails to build on leanprover/lean4:v4.27.0
    Velvet
  2. Commit 6e27c1b builds on the old leanprover/lean4:v4.26.0
    PartialRegularity
    Lean formalizations for the paper "Almost all primes are partially regular"
  3. Commit 3b00bde builds on the old leanprover/lean4:v4.26.0
    Deadends
  4. 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.
  5. Commit 5760d61 builds on the recent leanprover/lean4:v4.28.0-rc1
    leansqlite
    SQLite bindings for Lean
  6. Commit 976c1d3 builds on the recent leanprover/lean4:v4.27.0-rc1
    qdt
    Query-based Dependent Type Elaborator
  7. Commit 250d2a8 builds on the recent leanprover/lean4:v4.28.0-rc1
    LeanBench
  8. Commit 315e099 builds on the old leanprover/lean4:v4.19.0
    LeanCat
    Lean4 benchmark on 1 category.
  9. Commit c177541 builds on the old leanprover/lean4:v4.24.0
    fineqs
    Lean4 formalization with Artistotle of the arXiv paper 1906.11174
  10. Commit c2d912e builds on the old leanprover/lean4:v4.26.0
    FelConjecture
    Lean formalizations for the paper "Fel's conjecture on syzigies of numerical semigroups"
All newly created

Recently Updated

  1. Commit f5a1c1f builds on the recent leanprover/lean4:v4.28.0-rc1
    bignum
    port of s2n-bignum to Lean
  2. Commit 432d7da builds on the old leanprover/lean4:v4.22.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  3. Commit b60c806 builds on the recent leanprover/lean4:v4.28.0-rc1
    PrimeNumberTheoremAnd
    Blueprint for the PNT+ Project
  4. Commit 2598404 builds on the recent leanprover/lean4:v4.28.0-rc1
    mathlib
    The math library of Lean 4
  5. Commit 48a4675 builds on the recent leanprover/lean4:v4.28.0-rc1
    compfiles
    Catalog Of Math Problems Formalized In Lean
  6. Commit 0ca7b1e builds on the recent leanprover/lean4:v4.27.0-rc1
    ray
    Formalizing results about the Mandelbrot set in Lean
  7. Commit d174c20 builds on the recent leanprover/lean4:v4.27.0-rc1
    Iwasawalib
    Formalization of Iwasawa Theory in LꓱꓯN (tentative)
  8. Commit e2a9274 builds on the old leanprover/lean4:v4.25.2
    ssreflect
    LeanSSR: an SSReflect-Like Tactic Language for Lean
  9. Commit 7991986 builds on the recent leanprover/lean4:v4.27.0
    Duper
  10. Commit 64ec75f builds on the old leanprover/lean4:v4.25.2
    Curve25519Dalek
    Verifying curve25519-dalek using Lean
All recently updated