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

No results found

Latest Lean Stable:

leanprover/lean4:v4.26.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 959c852 builds on the recent leanprover/lean4:v4.27.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 6cd705a builds on the recent leanprover/lean4:v4.26.0-rc2 after lake update
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  4. Commit b062181 builds on the recent leanprover/lean4:v4.27.0-rc1
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  5. Commit 4fdc296 builds on the old leanprover/lean4:v4.22.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  6. Commit fea2a7c builds on the recent leanprover/lean4:v4.27.0-rc1 after lake update
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  7. Commit 5e46624 builds on the old leanprover/lean4:v4.20.1
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  8. Commit 53f112d builds on the old leanprover/lean4:v4.15.0-rc1
    scilean
    Scientific computing in Lean 4
  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 6379724 builds on the recent leanprover/lean4:v4.26.0
    PhysLean
    A project to digitalise results from physics into Lean.
All most popular

Newly Created

  1. Commit c177541 builds on the old leanprover/lean4:v4.24.0
    fineqs
    Lean4 formalization with Artistotle of the arXiv paper 1906.11174
  2. Commit 7845af8 builds on the recent leanprover/lean4:v4.26.0
    LeanLangur
    Expositions and demos for Lean Prover
  3. Commit 833a206 builds on the old leanprover/lean4:v4.24.0
    ZeroToQED
    From Zero to QED: An informal introduction to formality with Lean 4
  4. Commit 5ac51d2 builds on the recent leanprover/lean4:v4.27.0-rc1 after lake update
    HexLuthor
    Lean 4 hex color syntax with inline VS Code color preview
  5. Commit 0dbb921 builds on the recent leanprover/lean4:v4.27.0-rc1 after lake update
    Putnam
  6. Commit a186100 builds on the recent leanprover/lean4:v4.27.0-rc1
    event-structures
    Formalisation of some facts about event structures and reversibility
  7. Commit f92d648 builds on the recent leanprover/lean4:v4.25.2
    sgc
    A formally verified Lean 4 library characterizing the algebraic structure of metastability and consolidation in stochastic systems.
  8. Commit ec8c147 builds on the recent leanprover/lean4:v4.26.0 after lake update
    clap
    Implementation of the Clap language for ZK Circuits in the Lean proof-assistant
  9. Commit 4922402 builds on the recent leanprover/lean4:v4.27.0-rc1
    Leanduction
    Generate good induction principles on nested inductive types
  10. Commit 226aa7d builds on the recent leanprover/lean4:v4.27.0-rc1 after lake update
    VerifiedGPU
All newly created

Recently Updated

  1. Commit ec8c147 builds on the recent leanprover/lean4:v4.26.0 after lake update
    clap
    Implementation of the Clap language for ZK Circuits in the Lean proof-assistant
  2. Commit 959c852 builds on the recent leanprover/lean4:v4.27.0-rc1
    mathlib
    The math library of Lean 4
  3. Commit 4fdc296 builds on the old leanprover/lean4:v4.22.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  4. Commit 7fc9d82 builds on the old leanprover/lean4:v4.24.0
    SemicircleLaw
    Formalization of Wigner's Semicircle Law in Lean
  5. Commit 0b2b7ce fails to build on leanprover/lean4:v4.27.0-rc1
    verso-manual
    The Lean reference manual
  6. Commit 833a206 builds on the old leanprover/lean4:v4.24.0
    ZeroToQED
    From Zero to QED: An informal introduction to formality with Lean 4
  7. Commit f7c1595 fails to build on leanprover/lean4:v4.27.0-rc1
    HopfieldNet
  8. Commit bc7b7f5 builds on the recent leanprover/lean4:v4.27.0-rc1
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  9. Commit c2f45a6 builds on the old leanprover/lean4:v4.24.0-rc1
    groebner
    Formalization of Gröbner basis theory in Lean4 (WIP)
  10. Commit 08a3b95 builds on the recent leanprover/lean4:v4.26.0 after lake update
    quasi-borel-spaces
    A formalization of Quasi-Borel Spaces in Lean 4
All recently updated