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

No results found

Latest Lean Stable:

leanprover/lean4:v4.21.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 c3f0f19 builds on the recent leanprover/lean4:v4.22.0-rc4
    mathlib
    The math library of Lean 4
  2. Commit 6196563 builds on the recent leanprover/lean4:v4.22.0-rc4
    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 7f15456 builds on the recent leanprover/lean4:v4.22.0-rc4
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  5. Commit a664912 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-rc4
    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 2f4bea7 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 3f34c24 builds on the recent leanprover/lean4:v4.22.0-rc4
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  10. Commit 3c35be2 builds on the recent leanprover/lean4:v4.21.0
    PhysLean
    A project to digitalise results from physics into Lean.
All most popular

Newly Created

  1. Commit 44733fb builds on the recent leanprover/lean4:v4.22.0-rc4
    ConvolutedProofs
    Absurdly sophisticated proofs of simple mathematical facts in Lean 4
  2. Commit f0dccdc fails to build on leanprover/lean4:v4.22.0-rc4
    Strata
  3. Commit 3c00332 builds on the recent leanprover/lean4:v4.22.0-rc4
    pol
    Proof of Lean: Formalizing Blockchain Fundamentals in Lean
  4. Commit d3abbc9 builds on the recent leanprover/lean4:v4.22.0-rc4
    software-foundations-lean
    📚 (WIP) Rewriting Software Foundations in Lean 4
  5. Commit 9a6f138 builds on the recent leanprover/lean4:v4.22.0-rc4
    ennreal-arith
    Arithmetic tactics for extended non-negative real numbers (ENNReal)
  6. Commit abdd5f4 builds on the recent leanprover/lean4:v4.22.0-rc3
    Numbers
    An introduction to numbers
  7. Commit 899e196 builds on the recent leanprover/lean4:v4.22.0-rc3
    riddle-proofs
    Riddles solved in Lean4 for educational purposes
  8. Commit cacc491 builds on the recent leanprover/lean4:v4.22.0-rc4
    cslib
    A Lean library for Computer Science
  9. Commit 0322377 builds on the recent leanprover/lean4:v4.21.0
    goose
    GOOSE in Lean4
  10. Commit c47c57a builds on the recent leanprover/lean4:v4.22.0-rc4
    tactic-programming-beginner-guide
    Beginner's guide to Tactic Programming in Lean
All newly created

Recently Updated

  1. Commit 64a6adb builds on the old leanprover/lean4:v4.19.0
    KLR
    A formalization of ML kernel languages
  2. Commit a664912 builds on the old leanprover/lean4:v4.17.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  3. Commit d32ca40 builds on the recent leanprover/lean4:v4.22.0-rc4
    verso
    Lean documentation authoring tool
  4. Commit 7f15456 builds on the recent leanprover/lean4:v4.22.0-rc4
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  5. Commit f554728 builds on the old leanprover/lean4:v4.17.0-rc1
    SSA
    A minimal development of SSA theory
  6. Commit ab5d685 builds on the recent leanprover/lean4:v4.22.0-rc4
    haskell-spec
    Formal specification of the Haskell Language Report
  7. Commit 3f34c24 builds on the recent leanprover/lean4:v4.22.0-rc4
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  8. Commit f0dccdc fails to build on leanprover/lean4:v4.22.0-rc4
    Strata
  9. Commit c3f0f19 builds on the recent leanprover/lean4:v4.22.0-rc4
    mathlib
    The math library of Lean 4
  10. Commit 3c35be2 builds on the recent leanprover/lean4:v4.21.0
    PhysLean
    A project to digitalise results from physics into Lean.
All recently updated