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 9da3d90 builds on the recent leanprover/lean4:v4.19.0-rc3
    mathlib
    The math library of Lean 4
  2. Commit 9498454 builds on the recent leanprover/lean4:v4.18.0
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  3. Commit 0fb99d8 builds on the recent leanprover/lean4:v4.19.0-rc3
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  4. Commit 2c9cad0 builds on the recent leanprover/lean4:v4.19.0-rc3
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  5. Commit 53f112d builds on the old leanprover/lean4:v4.15.0
    scilean
    Scientific computing in Lean 4
  6. Commit bc6dc1e builds on the old leanprover/lean4:v4.14.0-rc3
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  7. Commit f523fcb builds on the recent leanprover/lean4:v4.19.0-rc3
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  8. Commit 323e9f0 builds on the recent leanprover/lean4:v4.19.0-rc3
    aesop
    White-box automation for Lean 4
  9. Commit 731400d builds on the recent leanprover/lean4:v4.19.0-rc3
    lean4-metaprogramming-book
  10. Commit 07da422 builds on the old leanprover/lean4:v4.5.0
    formalising-mathematics-2024
    Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.

Newly Created

  1. Commit 078a0db builds on the recent leanprover/lean4:v4.19.0-rc3
    kimina
    A Lean tactic that invokes the Kimina Prover Preview model to offer proof suggestions.
  2. Commit 3118411 builds on the recent leanprover/lean4:v4.19.0-rc3
    cryptolib
  3. Commit 02f8d14 builds on the recent leanprover/lean4:v4.18.0-rc1
    LeanTeX_Mathlib
    LeanTeX pretty printers for mathlib
  4. Commit 6e27ac1 builds on the recent leanprover/lean4:v4.18.0-rc1
    NeuralNetworks
    Formalization of Neural Networks in Lean 4
  5. Commit c4586f5 builds on the recent leanprover/lean4:v4.18.0-rc1
    combinatorial-games
    Combinatorial game library in Lean 4
  6. Commit 0be2cbd fails to build on leanprover/lean4:v4.19.0-rc3
    lean4-analysis-tao
    Formalization of "Analysis I" by Terence Tao
  7. Commit 75d0dab fails to build on leanprover/lean4:v4.19.0-rc3
    sqlite
    Sqlite3 bindings for lean4
  8. Commit ecdde79 builds on the recent leanprover/lean4:v4.18.0-rc1
    LeanBanachTarski
  9. Commit c4f495b builds on the recent leanprover/lean4:v4.19.0-rc3
    Toric
    Formalisation of toric varieties in Lean 4
  10. Commit 7fd55ea fails to build on leanprover/lean4:v4.18.0
    formalising-mathematics
    Course on theorem proving with Lean

Recently Updated

  1. Commit 750cc34 fails to build on leanprover/lean4:v4.19.0-rc3
    LeanLJ
    Lennard Jones in Lean
  2. Commit 9da3d90 builds on the recent leanprover/lean4:v4.19.0-rc3
    mathlib
    The math library of Lean 4
  3. Commit 7ce8ddd builds on the recent leanprover/lean4:v4.18.0
    KLR
    A formalization of ML kernel languages
  4. Commit a186683 builds on the recent leanprover/lean4:v4.18.0
    VCVio
    Formalized Cryptography Proofs in Lean 4
  5. Commit c4f495b builds on the recent leanprover/lean4:v4.19.0-rc3
    Toric
    Formalisation of toric varieties in Lean 4
  6. Commit 9498454 builds on the recent leanprover/lean4:v4.18.0
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  7. Commit 236d583 builds on the recent leanprover/lean4:v4.18.0-rc1
    pdl
    Tableaux for Propositional Dynamic Logic in Lean 4 (WORK IN PROGRESS)
  8. Commit 991d95d builds on the recent leanprover/lean4:v4.18.0
    Zklib
    Formally Verified SNARKs in Lean
  9. Commit 8582a62 builds on the recent leanprover/lean4:v4.19.0-rc3
    carleson
    A formalized proof of Carleson's theorem in Lean
  10. Commit 9cfd9cd builds on the recent leanprover/lean4:v4.19.0-rc3
    Matroid