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 fb23240 builds on the recent leanprover/lean4:v4.14.0-rc2
    mathlib
    The math library of Lean 4
  2. Commit f6a3f14 builds on the old leanprover/lean4:v4.11.0
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  3. Commit e2b76ee builds on the recent leanprover/lean4:v4.14.0-rc2
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  4. Commit 92b1246 builds on the recent leanprover/lean4:v4.14.0-rc2
    scilean
    Scientific computing in Lean 4
  5. Commit f56857a builds on the recent leanprover/lean4:v4.14.0-rc2
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  6. Commit 01f4969 builds on the recent leanprover/lean4:v4.14.0-rc2
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  7. Commit 3f28838 builds on the old leanprover/lean4:v4.7.0
    lean4-metaprogramming-book
  8. Commit 9a7479f builds on the recent leanprover/lean4:v4.14.0-rc2
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  9. Commit de91b59 builds on the recent leanprover/lean4:v4.14.0-rc2
    aesop
    White-box automation for Lean 4
  10. Commit 80f5638 builds on the recent leanprover/lean4:v4.14.0-rc2
    ntptutorial
    Tutorial on neural theorem proving

Newly Created

  1. Commit d7f2512 builds on the recent leanprover/lean4:v4.14.0-rc2
    CodeProofTheArena
    Lean coding problem solving challenge website with proof verification
  2. Commit 9f3241a builds on the recent leanprover/lean4:v4.14.0-rc2
    remco-mul
  3. Commit c90caa1 builds on the recent leanprover/lean4:v4.14.0-rc2
    order-pq
    Lean formalisation of the classification of the groups of order `p * q` where `p` and `q` are prime numbers.
  4. Commit 256986c builds on the recent leanprover/lean4:v4.13.0
    borel_det
  5. Commit 42dc02b builds on the recent leanprover/lean4:v4.14.0-rc2
    plausible
  6. Commit 8e24b93 builds on the recent leanprover/lean4:v4.13.0-rc4
    FMCn_Lean
    Repositório destinado às práticas de Lean4 da Monitoria de FMCn.
  7. Commit 5ae790f builds on the recent leanprover/lean4:v4.13.0-rc4
    Seminar
    Past contents of Lean Seminars in Bonn
  8. Commit c5d60b8 builds on the recent leanprover/lean4:v4.14.0-rc2
    LeanSudoku
    Playing Sudoku in the Lean 4 proof assistant
  9. Commit cfdc916 builds on the recent leanprover/lean4:v4.14.0-rc2
    Seymour
  10. Commit be2e471 builds on the recent leanprover/lean4:v4.14.0-rc2
    ExFormMathL4

Recently Updated

  1. Commit fb23240 builds on the recent leanprover/lean4:v4.14.0-rc2
    mathlib
    The math library of Lean 4
  2. Commit b9fffc6 builds on the recent leanprover/lean4:v4.14.0-rc2
    carleson
    A formalized proof of Carleson's theorem in Lean
  3. Commit 059eb7e builds on the recent leanprover/lean4:v4.14.0-rc2
    doc-gen4
    Document Generator for Lean 4
  4. Commit 01f4969 builds on the recent leanprover/lean4:v4.14.0-rc2
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  5. Commit ec3e131 builds on the old leanprover/lean4:nightly
    NKL
    A formalization of the NKI ISA
  6. Commit 70a3b6a builds on the recent leanprover/lean4:v4.14.0-rc2
    compfiles
    Catalog Of Math Problems Formalized In Lean
  7. Commit 9fa4177 builds on the recent leanprover/lean4:v4.14.0-rc2
    LeanCourse
    Bonn Lean course for winter 24/25
  8. Commit 628c142 fails to build on leanprover/lean4:v4.14.0-rc2
    GameTheory
  9. Commit 42dc02b builds on the recent leanprover/lean4:v4.14.0-rc2
    plausible
  10. Commit 26bcae6 builds on the recent leanprover/lean4:v4.14.0-rc2
    proofwidgets
    Helper toolkit for creating your own Lean 4 UserWidgets