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

No results found

Latest Lean Stable:

leanprover/lean4:v4.33.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 ffa6ef0 builds on the recent leanprover/lean4:v4.34.0-rc1
    mathlib
    The math library of Lean 4
  2. Commit 8f9e0fc 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.34.0-rc1
    ryu
    Converts floating point numbers to decimal strings
  4. Commit 2458f73 builds on the recent leanprover/lean4:v4.34.0-rc1 after lake update
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  5. Commit 4010c1f builds on the old leanprover/lean4:v4.27.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  6. Commit e99f167 builds on the recent leanprover/lean4:v4.34.0-rc1
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit a7a6d46 builds on the old leanprover/lean4:v4.32.0
    Physlib
    A project to digitalise results from physics into Lean.
  8. Commit f5c73b0 builds on the recent leanprover/lean4:v4.34.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 54edcda 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 0d2b3b5 builds on the recent leanprover/lean4:v4.32.1
    gonzalgo
    Write out the declaration graph of a Lean environment, statement dependencies kept apart from proof dependencies, so you can find what a theorem actually rests on.
  2. Commit 4d305b9 builds on the recent leanprover/lean4:v4.32.1
    lean-tee
    Lean-specified zkTEE: measured guest execution, hashed receipts, lean-grpc APIs
  3. Commit 0887548 builds on the recent leanprover/lean4:v4.32.1
    lean-grpc
    Pure Lean 4 gRPC stack (HTTP/2 + HPACK + gRPC) on Std.Async
  4. Commit 07ed6f9 builds on the recent leanprover/lean4:v4.33.0-rc1
    AutoGeneralization
    Kernel-checked theorem generalization for Lean
  5. Commit a4ca5ad fails to build on leanprover/lean4:v4.32.1
    Calculus_21
    An Universe for Mitar —— Classical Calculus
  6. 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
  7. Commit c789440 builds on the recent leanprover/lean4:v4.33.0-rc1
    descriptive-complexity
    Descriptive complexity in Lean 4: machine-model-free NP-completeness via first-order reductions, and the polynomial hierarchy via second-order alternation
  8. 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.
  9. Commit 8f2ee54 builds on the old 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).
  10. Commit 5c667c3 builds on the recent leanprover/lean4:v4.32.2
    domain-theory
    A Lean Library for Domain Theory
All newly created

Recently Updated

  1. Commit f4416f8 builds on the recent leanprover/lean4:v4.33.0
    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 a5fc584 builds on the recent leanprover/lean4:v4.34.0-rc1
    beam
    Claude/Codex skill and local workflow layer for efficient interaction with Lean 4 and Monte-Carlo Tree Search.
  3. Commit bd78196 builds on the old leanprover/lean4:v4.29.1
    ix
    a zero-knowledge proof-carrying code platform for Lean 4
  4. Commit 0b90bc4 builds on the recent leanprover/lean4:v4.33.0-rc1
    Hex
    Development monorepo for Hex: verified computational algebra in Lean 4 (polynomial factoring, LLL, and friends). Released aggregate: https://github.com/leanprover/hex
  5. Commit 70c3d23 builds on the recent leanprover/lean4:v4.34.0-rc1
    TauCeti
    An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics
  6. Commit 9ea9174 builds on the recent leanprover/lean4:v4.33.0-rc1
    foam
    geometry of hospitality
  7. Commit ffa6ef0 builds on the recent leanprover/lean4:v4.34.0-rc1
    mathlib
    The math library of Lean 4
  8. Commit eead15f builds on the old leanprover/lean4:v4.30.0-rc2 after lake update
    EvmAsm
  9. Commit 40e6a9b builds on the old leanprover/lean4:v4.31.0
    Arklib
    Formally Verified Arguments of Knowledge in Lean
  10. Commit 4010c1f builds on the old leanprover/lean4:v4.27.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
All recently updated