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 8dbc02d builds on the recent leanprover/lean4:v4.29.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 4c0618b fails to build on leanprover/lean4:v4.28.0
    ryu
    Converts floating point numbers to decimal strings
  4. Commit bbecd66 builds on the recent leanprover/lean4:v4.28.0
    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 2b8748e builds on the recent leanprover/lean4:v4.28.0-rc1
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit c901c54 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.28.0 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 9a61202 builds on the old leanprover/lean4:v4.24.0
    Velvet
    An auto-active verifier embedded into Lean
  2. 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
  3. Commit 4aa3287 builds on the recent leanprover/lean4:v4.28.0
    Coinductive
    Co-inductive datatypes for Lean
  4. Commit 6e27c1b builds on the old leanprover/lean4:v4.26.0
    PartialRegularity
    Lean formalizations for the paper "Almost all primes are partially regular"
  5. Commit 3b00bde builds on the old leanprover/lean4:v4.26.0
    Deadends
  6. Commit e1f334f builds on the recent leanprover/lean4:v4.28.0
    tvm-lean
  7. Commit 2fa1384 builds on the recent leanprover/lean4:v4.28.0
    MRiscX
    A certified RISC-V Interpreter with Hoare-logic in Lean
  8. Commit 625d8f5 builds on the recent leanprover/lean4:v4.28.0
    sparkle
    A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.
  9. Commit 2765af4 builds on the recent leanprover/lean4:v4.28.0
    leansqlite
    SQLite bindings for Lean
  10. Commit 2b4e3ad builds on the old leanprover/lean4:v4.27.0-rc1
    qdt
    Query-based Dependent Type Elaborator
All newly created

Recently Updated

  1. Commit 8dbc02d builds on the recent leanprover/lean4:v4.29.0-rc1
    mathlib
    The math library of Lean 4
  2. Commit 28175a8 builds on the recent leanprover/lean4:v4.28.0
    PrimeNumberTheoremAnd
    Blueprint for the PNT+ Project
  3. Commit f777606 builds on the old leanprover/lean4:v4.27.0
    SpherePacking
    A Lean formalisation of Maryna Viazovska's Fields Medal-winning solution to the sphere packing problem in dimension 8.
  4. Commit 77d1057 builds on the recent leanprover/lean4:v4.29.0-rc1
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  5. Commit 78a90cf builds on the recent leanprover/lean4:v4.28.0
    CompPoly
    A computable model of Polynomials in Lean.
  6. Commit 52efcac builds on the recent leanprover/lean4:v4.29.0-rc1
    compfiles
    Catalog Of Math Problems Formalized In Lean
  7. Commit 3d91ad1 builds on the old leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  8. Commit 6f67113 builds on the recent leanprover/lean4:v4.28.0
    Strata
  9. Commit e1f334f builds on the recent leanprover/lean4:v4.28.0
    tvm-lean
  10. Commit b212fa4 builds on the old leanprover/lean4:v4.18.0
    vcsp
    General-Valued Constraint Satisfaction Problems
All recently updated