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

No results found

Latest Lean Stable:

leanprover/lean4:v4.22.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 ee1b32b builds on the recent leanprover/lean4:v4.23.0-rc2
    mathlib
    The math library of Lean 4
  2. Commit 893a7f7 builds on the recent leanprover/lean4:v4.23.0-rc2
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  3. Commit 3d91ad1 builds on the old leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  4. Commit 55bdd4d builds on the recent leanprover/lean4:v4.23.0-rc2
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  5. Commit bf61426 builds on the old leanprover/lean4:v4.17.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  6. Commit e81dc5f builds on the recent leanprover/lean4:v4.22.0 after lake update
    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 9e0e8b7 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 2bf0e10 builds on the old leanprover/lean4:v4.21.0
    mil
    The user home repository for the Mathematics in Lean tutorial.
  10. Commit 76408f0 builds on the recent leanprover/lean4:v4.23.0-rc2
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
All most popular

Newly Created

  1. Commit 2ac8046 fails to build on leanprover/lean4:v4.23.0-rc2
    Physicslib
    Solving Hilbert's sixth problem in Lean
  2. Commit a8c05ba builds on the old leanprover/lean4:v4.20.1
    functorio
  3. Commit c06fce3 builds on the recent leanprover/lean4:v4.23.0-rc2
    render
    Verified renders of the Mandelbrot set
  4. Commit fee1e19 builds on the old leanprover/lean4:v4.16.0
    FATE-H
    The FATE-H (Formal Algebra Theorem Evaluation-Hard) benchmark.
  5. Commit 44733fb builds on the recent leanprover/lean4:v4.22.0 after lake update
    ConvolutedProofs
    Absurdly sophisticated proofs of simple mathematical facts in Lean 4
  6. Commit fd1fbd1 fails to build on leanprover/lean4:v4.23.0-rc2
    Strata
  7. Commit 3c00332 builds on the recent leanprover/lean4:v4.22.0 after lake update
    pol
    Proof of Lean: Formalizing Blockchain Fundamentals in Lean
  8. Commit d3abbc9 builds on the recent leanprover/lean4:v4.23.0-rc2
    software-foundations-lean
    📚 (WIP) Rewriting Software Foundations in Lean 4
  9. Commit 9212b89 builds on the old leanprover/lean4:v4.15.0
    lib
    Solving Competition Geometry Problems in Lean
  10. Commit 6af1ae9 builds on the recent leanprover/lean4:v4.23.0-rc2
    EllipticCurve
    Towards a general definition of elliptic curve over schemes
All newly created

Recently Updated

  1. Commit fd1fbd1 fails to build on leanprover/lean4:v4.23.0-rc2
    Strata
  2. Commit f554728 builds on the old leanprover/lean4:v4.17.0-rc1
    SSA
    A minimal development of SSA theory
  3. Commit ee1b32b builds on the recent leanprover/lean4:v4.23.0-rc2
    mathlib
    The math library of Lean 4
  4. Commit 9a06cc5 builds on the recent leanprover/lean4:v4.22.0-rc2
    Arklib
    Formally Verified Arguments of Knowledge in Lean
  5. Commit d4275eb builds on the old leanprover/lean4:v4.13.0
    itertools
    A Lean 4 library for iterators.
  6. Commit 1f046cf builds on the recent leanprover/lean4:v4.22.0
    glimpseOfLean
    An introduction to theorem proving in Lean for the impatient.
  7. Commit 2381be7 builds on the recent leanprover/lean4:v4.23.0-rc2
    compfiles
    Catalog Of Math Problems Formalized In Lean
  8. Commit 11a5a3d builds on the recent leanprover/lean4:v4.22.0
    VCVio
    Formalized Cryptography Proofs in Lean 4
  9. Commit 64a6adb builds on the old leanprover/lean4:v4.19.0
    KLR
    A formalization of ML kernel languages
  10. Commit b85db50 builds on the old leanprover/lean4:v4.21.0
    goose
    GOOSE in Lean4
All recently updated