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 84542b3 builds on the recent leanprover/lean4:v4.10.0-rc2
    mathlib
    The math library of Lean 4
  2. Commit 91dbe27 builds on the recent leanprover/lean4:v4.10.0-rc2
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  3. Commit f53f5a5 builds on the recent leanprover/lean4:v4.10.0-rc2
    examples
    Lean theorem proving interface which feels like pen-and-paper proofs.
  4. Commit aad7ae1 builds on the recent leanprover/lean4:v4.9.1
    scilean
    Scientific computing in Lean 4
  5. Commit f27beb1 builds on the recent leanprover/lean4:v4.10.0-rc2
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  6. Commit 4ffaf96 builds on the old leanprover/lean4:v4.7.0
    lean4-metaprogramming-book
  7. Commit 622d52c builds on the recent leanprover/lean4:v4.10.0-rc2
    aesop
    White-box automation for Lean 4
  8. Commit f7fc80f builds on the recent leanprover/lean4:v4.10.0-rc2
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  9. Commit 80f5638 builds on the recent leanprover/lean4:v4.10.0-rc2 after lake update
    ntptutorial
    Tutorial on neural theorem proving
  10. Commit 44ddc83 builds on the old leanprover/lean4:v4.8.0
    PrimeNumberTheoremAnd
    blueprint for prime number theorem and more

Newly Created

  1. Commit 5e45c1b fails to build on leanprover/lean4:v4.10.0-rc2
    HadwigerNelson
    Hadwiger-Nelson Problem Formalization in Lean 4
  2. Commit ff7808b fails to build on leanprover/lean4:v4.10.0-rc2
    lffi
  3. Commit 2ca670d builds on the old leanprover/lean4:v4.7.0
    Game
  4. Commit 64d3e1f builds on the recent leanprover/lean4:v4.10.0-rc2
    jixia
    A static analysis tool for Lean 4.
  5. Commit f1912c3 builds on the old leanprover/lean4:v4.8.0
    lib
    LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.
  6. Commit 0be7902 builds on the old leanprover/lean4:v4.8.0
    ray
    Conservative floating point interval arithmetic in Lean
  7. Commit dbca34c builds on the recent leanprover/lean4:v4.10.0-rc2
    DGAlgorithms
    Distributed Graph Algorithms in Lean
  8. Commit ac65108 builds on the recent leanprover/lean4:v4.10.0-rc2
    Koch
    Koch 2D snowflake generator for 4D Golf
  9. Commit 383c641 builds on the recent leanprover/lean4:v4.10.0-rc2
    use-lean-standard-action-with-bare-project
  10. Commit d64165e builds on the recent leanprover/lean4:v4.10.0-rc2
    workshop
    Repo for the first BerLean workshop.

Recently Updated

  1. Commit 84542b3 builds on the recent leanprover/lean4:v4.10.0-rc2
    mathlib
    The math library of Lean 4
  2. Commit 079cac5 builds on the recent leanprover/lean4:v4.10.0-rc2
    flt-regular
    Fermat's Last Theorem for regular primes
  3. Commit 2cf7679 builds on the recent leanprover/lean4:v4.10.0-rc2
    compfiles
    Catalog Of Math Problems Formalized In Lean
  4. Commit f27beb1 builds on the recent leanprover/lean4:v4.10.0-rc2
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  5. Commit 0b5119f builds on the old leanprover/lean4:v4.7.0
    leansec
    Total parser combinators library for Lean4
  6. Commit 3c7b7a4 builds on the recent leanprover/lean4:v4.10.0-rc2
    Lean by Example
    コード例で学ぶ Lean 言語
  7. Commit 9b9fc9d builds on the recent leanprover/lean4:v4.10.0-rc2 after lake update
    SSA
    A minimal development of SSA theory
  8. Commit aa936ae builds on the recent leanprover/lean4:v4.10.0-rc2
    testing_lower_bounds
    Lower bounds for hypothesis testing and estimation, in Lean
  9. Commit b653201 builds on the recent leanprover/lean4:v4.10.0-rc2
    sampcert
    SampCert : Verified Differential Privacy
  10. Commit 71c9e16 builds on the recent leanprover/lean4:v4.9.1
    matroid