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

No results found

Latest Lean Stable:

leanprover/lean4:v4.27.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 23d606e builds on the recent leanprover/lean4:v4.27.0 after lake update
    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 old leanprover/lean4:v4.26.0-rc2 after lake update
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  4. Commit 782d8b9 builds on the recent leanprover/lean4:v4.27.0
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  5. Commit f218287 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 after lake update
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  7. Commit 4de9edc 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 fcf2471 builds on the old leanprover/lean4:v4.26.0
    PhysLean
    A project to digitalise results from physics into Lean.
  9. Commit 53f112d builds on the old leanprover/lean4:v4.15.0-rc1
    scilean
    Scientific computing in Lean 4
  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 c19c977 builds on the recent leanprover/lean4:v4.27.0
    leansqlite
    SQLite bindings for Lean
  2. Commit 5b3df42 builds on the recent leanprover/lean4:v4.27.0-rc1
    qdt
    Query-based Dependent Type Elaborator
  3. Commit 923bb91 builds on the old leanprover/lean4:v4.19.0
    LeanCat
    Lean4 benchmark on 1 category.
  4. Commit c177541 builds on the old leanprover/lean4:v4.24.0
    fineqs
    Lean4 formalization with Artistotle of the arXiv paper 1906.11174
  5. Commit b542606 builds on the old leanprover/lean4:v4.26.0
    LeanLangur
    Expositions and demos for Lean Prover
  6. Commit 9beebd8 builds on the old leanprover/lean4:v4.26.0
    ZeroToQED
    From Zero to QED: An informal introduction to formality with Lean 4
  7. Commit 5ac51d2 builds on the recent leanprover/lean4:v4.27.0 after lake update
    HexLuthor
    Lean 4 hex color syntax with inline VS Code color preview
  8. Commit 0dbb921 builds on the recent leanprover/lean4:v4.27.0-rc1 after lake update
    Putnam
  9. Commit a186100 builds on the recent leanprover/lean4:v4.27.0-rc1
    event-structures
    Formalisation of some facts about event structures and reversibility
  10. Commit e49e1f2 builds on the old leanprover/lean4:v4.25.2
    sgc
    Lean 4 library characterizing the algebraic structure of metastability and consolidation in stochastic systems
All newly created

Recently Updated

  1. Commit 6254bed builds on the recent leanprover/lean4:v4.27.0-rc1
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  2. Commit 09dd03b builds on the old leanprover/lean4:v4.24.0
    ix
    a zero-knowledge proof-carrying code platform for Lean 4
  3. Commit 361b3a1 builds on the old leanprover/lean4:v4.26.0
    Heights
    An attempt at formalizing the theory of heights in Lean
  4. Commit 46b9e7f fails to build on leanprover/lean4:v4.27.0
    CompPoly
    A computable model of Polynomials in Lean.
  5. Commit 23d606e builds on the recent leanprover/lean4:v4.27.0 after lake update
    mathlib
    The math library of Lean 4
  6. Commit 24832ec builds on the recent leanprover/lean4:v4.27.0 after lake update
    IMOSLLean4
    Formalization of IMO shortlist problems in Lean 4
  7. Commit 3832604 builds on the recent leanprover/lean4:v4.27.0-rc1
    LeanBandits
    Bandit algorithms in Lean
  8. Commit 8d4b899 builds on the recent leanprover/lean4:v4.27.0 after lake update
    VD
    Formalizing Value Distribution Theory
  9. Commit 909478b builds on the recent leanprover/lean4:v4.27.0
    soma-workspace
    ⚗️ | λC pure functional language with deterministic, GC-free memory via Interaction Nets and automatic parallelism.
  10. Commit 989447b builds on the recent leanprover/lean4:v4.27.0-rc1
    Foundation
    Formalization of Mathematical Logic
All recently updated