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

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 171b569 builds on the recent leanprover/lean4:v4.22.0-rc3
    mathlib
    The math library of Lean 4
  2. Commit 6196563 builds on the recent leanprover/lean4:v4.22.0-rc3
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  3. Commit 3d91ad1 builds on the recent leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  4. Commit 1eefe02 builds on the old leanprover/lean4:v4.17.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  5. Commit abe9a60 builds on the recent leanprover/lean4:v4.22.0-rc3
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  6. Commit c5a3e62 builds on the recent leanprover/lean4:v4.22.0-rc3
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  7. Commit 53f112d builds on the old leanprover/lean4:v4.15.0-rc1
    scilean
    Scientific computing in Lean 4
  8. Commit 5490062 builds on the recent leanprover/lean4:v4.20.1
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  9. Commit 82fd0cf builds on the recent leanprover/lean4:v4.22.0-rc3
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  10. Commit a763c59 builds on the recent leanprover/lean4:v4.21.0
    PhysLean
    A project to digitalise results from physics into Lean.

Recently Updated

  1. Commit 61b75ff builds on the recent leanprover/lean4:v4.22.0-rc3
    carleson
    A formalized proof of Carleson's theorem in Lean
  2. Commit 171b569 builds on the recent leanprover/lean4:v4.22.0-rc3
    mathlib
    The math library of Lean 4
  3. Commit a763c59 builds on the recent leanprover/lean4:v4.21.0
    PhysLean
    A project to digitalise results from physics into Lean.
  4. Commit 64a6adb builds on the old leanprover/lean4:v4.19.0
    KLR
    A formalization of ML kernel languages
  5. Commit ff89a04 builds on the recent leanprover/lean4:v4.22.0-rc3
    haskell-spec
    Formal specification of the Haskell Language Report
  6. Commit 93455f3 builds on the recent leanprover/lean4:v4.21.0
    iris
    Lean 4 port of Iris, a higher-order concurrent separation logic framework
  7. Commit 9705fd4 builds on the old leanprover/lean4:v4.18.0
    ix
    a zero-knowledge proof-carrying code platform for Lean 4
  8. Commit 14c5b1f builds on the recent leanprover/lean4:v4.22.0-rc3
    Matroid
  9. Commit 82fd0cf builds on the recent leanprover/lean4:v4.22.0-rc3
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  10. Commit 1eefe02 builds on the old leanprover/lean4:v4.17.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.