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 74ac4b5 builds on the recent leanprover/lean4:v4.20.0
    mathlib
    The math library of Lean 4
  2. Commit 8c91154 builds on the recent leanprover/lean4:v4.20.0
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  3. Commit 152f1b4 builds on the recent leanprover/lean4:v4.20.0-rc5
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  4. Commit 7f9ec4e builds on the old leanprover/lean4:v4.17.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  5. Commit 164b8db builds on the recent leanprover/lean4:v4.20.0
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  6. Commit 53f112d builds on the old leanprover/lean4:v4.15.0
    scilean
    Scientific computing in Lean 4
  7. Commit 1c29672 builds on the recent leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  8. Commit 7779c23 builds on the recent leanprover/lean4:v4.20.0
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  9. Commit 233a67f builds on the recent leanprover/lean4:v4.20.0-rc5
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  10. Commit c548baa builds on the recent leanprover/lean4:v4.20.0
    aesop
    White-box automation for Lean 4

Newly Created

  1. Commit 1c29672 builds on the recent leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  2. Commit 3c0efe0 builds on the old leanprover/lean4:v4.19.0
    Lie
    A classification theorem in Lean of solvable Lie algebras of dimension zero to three
  3. Commit 5ec9f03 builds on the old leanprover/lean4-pr-releases:pr-release-8003
    mini-redis
    An implementation of mini-redis in Lean 4
  4. Commit 6866f29 builds on the old leanprover/lean4:v4.18.0
    verina
  5. Commit d1d2a02 builds on the recent leanprover/lean4:v4.20.0
    SemicircleLaw
    Formalization of Wigner's Semicircle Law in Lean
  6. Commit 7f9ec4e builds on the old leanprover/lean4:v4.17.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  7. Commit b8d0cec builds on the old leanprover/lean4:v4.19.0
    bruhat-tits
    A formalisation of the Bruhat-Tits tree in Lean4
  8. Commit 90fd935 builds on the recent leanprover/lean4:v4.20.0
    LeanPlot
  9. Commit 52447ae builds on the recent leanprover/lean4:v4.20.0-rc5
    logic-formalization
    Formalize "Logic Notes" by Lou van den Dries in Lean
  10. Commit 156e3b2 builds on the recent leanprover/lean4:v4.20.0
    rupert
    Formalization of the Rupert Problem for convex polyhedra.

Recently Updated

  1. Commit 74ac4b5 builds on the recent leanprover/lean4:v4.20.0
    mathlib
    The math library of Lean 4
  2. Commit 1c29672 builds on the recent leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  3. Commit 7f4d327 builds on the old leanprover/lean4:v4.19.0
    Clean
    Lean circuit DSL
  4. Commit b8b19c7 builds on the recent leanprover/lean4:v4.20.0
    carleson
    A formalized proof of Carleson's theorem in Lean
  5. Commit f554728 builds on the old leanprover/lean4:v4.17.0-rc1
    SSA
    A minimal development of SSA theory
  6. Commit 152f1b4 builds on the recent leanprover/lean4:v4.20.0-rc5
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit 989b94b builds on the recent leanprover/lean4:v4.20.0-rc5
    ABCExceptions
    Exceptions to the ABC conjecture in Lean
  8. Commit 7f9ec4e builds on the old leanprover/lean4:v4.17.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  9. Commit 7518aca builds on the recent leanprover/lean4:v4.20.0
    proofwidgets
    Helper toolkit for creating your own Lean 4 UserWidgets
  10. Commit 233a67f builds on the recent leanprover/lean4:v4.20.0-rc5
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover