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

No results found

Latest Lean Stable:

leanprover/lean4:v4.23.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 2b4a36b builds on the recent leanprover/lean4:v4.23.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 a26e113 builds on the recent leanprover/lean4:v4.23.0
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  4. Commit a8ff033 builds on the recent leanprover/lean4:v4.23.0-rc2
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  5. Commit bbebc54 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.23.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 c106b7a 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 8cf1509 builds on the recent leanprover/lean4:v4.23.0
    PhysLean
    A project to digitalise results from physics into Lean.
All most popular

Newly Created

  1. Commit 4e0afdf fails to build on leanprover/lean4:v4.23.0
    LeanDoomed
    Simple Raycasting Example in Lean4 using SDL3
  2. Commit 2ac8046 fails to build on leanprover/lean4:v4.23.0
    Physicslib
    Solving Hilbert's sixth problem in Lean
  3. Commit 6f32f59 builds on the old leanprover/lean4:v4.20.1
    functorio
  4. Commit 3f108f7 builds on the recent leanprover/lean4:v4.23.0-rc2
    Game
    RealAnalysisGame
  5. Commit c06fce3 builds on the recent leanprover/lean4:v4.23.0-rc2
    render
    Verified renders of the Mandelbrot set
  6. Commit fee1e19 builds on the recent leanprover/lean4:v4.23.0 after lake update
    FATE-H
    The FATE-H (Formal Algebra Theorem Evaluation-Hard) benchmark.
  7. 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
  8. Commit d051c6f fails to build on leanprover/lean4:v4.23.0
    Strata
  9. Commit c71ce23 builds on the recent leanprover/lean4:v4.23.0 after lake update
    pol
    Proof of Lean: Formalizing Blockchain Fundamentals in Lean
  10. Commit d3abbc9 builds on the recent leanprover/lean4:v4.23.0
    software-foundations-lean
    📚 (WIP) Rewriting Software Foundations in Lean 4
All newly created

Recently Updated

  1. Commit f554728 builds on the old leanprover/lean4:v4.17.0-rc1
    SSA
    A minimal development of SSA theory
  2. Commit 2b4a36b builds on the recent leanprover/lean4:v4.23.0 after lake update
    mathlib
    The math library of Lean 4
  3. Commit d051c6f fails to build on leanprover/lean4:v4.23.0
    Strata
  4. Commit 537f03a builds on the recent leanprover/lean4:v4.22.0
    goose
    GOOSE in Lean4
  5. Commit 5583dfb builds on the recent leanprover/lean4:v4.23.0
    haskell-spec
    Formal specification of the Haskell Language Report
  6. Commit c205f53 builds on the recent leanprover/lean4:v4.23.0
    plausible
  7. Commit 3558f5b builds on the recent leanprover/lean4:v4.22.0
    Game
    Natural Number Game
  8. Commit c8da0f3 builds on the recent leanprover/lean4:v4.23.0
    VD
    Formalizing Value Distribution Theory
  9. Commit 6e89c73 builds on the recent leanprover/lean4:v4.23.0-rc2
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  10. Commit e10f63a builds on the recent leanprover/lean4:v4.23.0-rc2
    Clean
    Lean circuit DSL
All recently updated