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 2642f52 builds on the recent leanprover/lean4:v4.21.0-rc3
    mathlib
    The math library of Lean 4
  2. Commit 2b2d590 builds on the recent leanprover/lean4:v4.21.0-rc3
    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 4665e8c builds on the old leanprover/lean4:v4.17.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  5. Commit 405fa59 builds on the recent leanprover/lean4:v4.21.0-rc3
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  6. Commit 902b97d builds on the recent leanprover/lean4:v4.21.0-rc3
    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 4de9edc 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 5e6a775 builds on the recent leanprover/lean4:v4.21.0-rc3
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  10. Commit c3a19fa builds on the recent leanprover/lean4:v4.21.0-rc3
    aesop
    White-box automation for Lean 4

Newly Created

  1. Commit 3d91ad1 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 312192d builds on the old leanprover/lean4-pr-releases:pr-release-8003
    mini-redis
    An implementation of mini-redis in Lean 4
  4. Commit d3d5bbf builds on the old leanprover/lean4:v4.18.0
    verina
    Verina (Verifiable Code Generation Arena) is a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions.
  5. Commit 9f0f43c builds on the recent leanprover/lean4:v4.21.0-rc3
    SemicircleLaw
    Formalization of Wigner's Semicircle Law in Lean
  6. Commit 7087b15 fails to build on leanprover/lean4:v4.21.0-rc3
    lie-classification
    Classification of Lie algebras in Lean
  7. Commit 4665e8c builds on the old leanprover/lean4:v4.17.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  8. Commit b8d0cec builds on the old leanprover/lean4:v4.19.0
    bruhat-tits
    A formalisation of the Bruhat-Tits tree in Lean4
  9. Commit 90fd935 builds on the recent leanprover/lean4:v4.21.0-rc3
    LeanPlot
  10. Commit 52447ae builds on the recent leanprover/lean4:v4.20.0-rc5
    logic-formalization
    Formalize "Logic Notes" by Lou van den Dries in Lean

Recently Updated

  1. Commit a32c42e builds on the old leanprover/lean4:v4.18.0
    ix
    a zero-knowledge proof-carrying code platform for Lean 4
  2. Commit 3d91ad1 builds on the recent leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  3. Commit a0a6806 builds on the recent leanprover/lean4:v4.21.0-rc3
    carleson
    A formalized proof of Carleson's theorem in Lean
  4. Commit 64a6adb builds on the old leanprover/lean4:v4.19.0
    KLR
    A formalization of ML kernel languages
  5. Commit 2642f52 builds on the recent leanprover/lean4:v4.21.0-rc3
    mathlib
    The math library of Lean 4
  6. Commit 5e6a775 builds on the recent leanprover/lean4:v4.21.0-rc3
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  7. Commit 405fa59 builds on the recent leanprover/lean4:v4.21.0-rc3
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  8. Commit fb52bde builds on the recent leanprover/lean4:v4.21.0-rc3
    BirkhoffErgodicThm
    A proof of Pointwise Birkhoff Ergodic Theorem in Lean
  9. Commit f554728 builds on the old leanprover/lean4:v4.17.0-rc1
    SSA
    A minimal development of SSA theory
  10. Commit d4367e8 builds on the recent leanprover/lean4:v4.21.0-rc3
    compfiles
    Catalog Of Math Problems Formalized In Lean