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 00d112f builds on the recent leanprover/lean4:v4.9.0-rc2
    mathlib
    The math library of Lean 4
  2. Commit fc83eef builds on the recent leanprover/lean4:v4.9.0-rc2 after lake update
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  3. Commit f53f5a5 builds on the recent leanprover/lean4:v4.9.0-rc2
    examples
    Lean theorem proving interface which feels like pen-and-paper proofs.
  4. Commit 9bfa80c builds on the recent leanprover/lean4:v4.9.0-rc2
    scilean
    Scientific computing in Lean 4
  5. Commit 73c7f46 builds on the recent leanprover/lean4:v4.9.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 882561b builds on the recent leanprover/lean4:v4.9.0-rc2
    aesop
    White-box automation for Lean 4
  8. Commit 80f5638 builds on the recent leanprover/lean4:v4.9.0-rc2 after lake update
    ntptutorial
    Tutorial on neural theorem proving
  9. Commit fbadcf5 builds on the recent leanprover/lean4:v4.9.0-rc2
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  10. Commit 44ddc83 builds on the recent leanprover/lean4:v4.8.0
    PrimeNumberTheoremAnd
    blueprint for prime number theorem and more

Newly Created

  1. Commit f1912c3 builds on the recent leanprover/lean4:v4.8.0
    lib
    LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.
  2. Commit ac65108 builds on the recent leanprover/lean4:v4.9.0-rc2
    Koch
    Koch 2D snowflake generator for 4D Golf
  3. Commit 5023145 builds on the recent leanprover/lean4:v4.9.0-rc2
    use-lean-standard-action-with-bare-project
  4. Commit 507fb66 builds on the recent leanprover/lean4:v4.8.0
    workshop
    Repo for the first BerLean workshop.
  5. Commit aed3615 builds on the recent leanprover/lean4:v4.9.0-rc2 after lake update
    quantumInfo
    Quantum information theory in Lean 4
  6. Commit dc05203 builds on the recent leanprover/lean4:v4.9.0-rc2
    LeanCondensed
  7. Commit 23495ea builds on the recent leanprover/lean4:v4.9.0-rc2
    hep_lean
    A project to digitalise results from high energy physics into Lean.
  8. Commit 8767940 builds on the recent leanprover/lean4:v4.9.0-rc2
    mathlib4-tactics
    List of the all tactics of mathlib4. This is heavily inspired by haruhisa-enomoto/mathlib4-all-tactics
  9. Commit 0b69f91 builds on the recent leanprover/lean4:v4.9.0-rc2
    bonnAnalysis
    repository for the collaborative formalization seminar in Analysis in Bonn
  10. Commit 7f9847f builds on the old leanprover/lean4:v4.7.0
    Game

Recently Updated

  1. Commit 00d112f builds on the recent leanprover/lean4:v4.9.0-rc2
    mathlib
    The math library of Lean 4
  2. Commit a503917 builds on the recent leanprover/lean4:v4.9.0-rc2
    Tactic Cheatsheet
    コード例で学ぶ Lean 言語
  3. Commit 73c7f46 builds on the recent leanprover/lean4:v4.9.0-rc2
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  4. Commit ffcaee2 builds on the recent leanprover/lean4:v4.9.0-rc2
    mathport
    Mathport is a tool for porting Lean3 projects to Lean4
  5. Commit 6e8f450 builds on the recent leanprover/lean4:v4.8.0
    IMOSLLean4
    Formalization of IMO shortlist problems in Lean 4
  6. Commit b70e585 builds on the recent leanprover/lean4:v4.8.0
    leancolls
    WIP collections library for Lean 4
  7. Commit 5b0251a builds on the recent leanprover/lean4:v4.9.0-rc2
    logic
    Lean4 Logic Formalization
  8. Commit ab2e4bb builds on the recent leanprover/lean4:v4.9.0-rc2
    cvc5
    A Foreign Function Interface (FFI) to cvc5 solver in Lean.
  9. Commit db8b80b builds on the recent leanprover/lean4:v4.9.0-rc2
    mdgen
    Tool to generate markdown files from lean files. This is heavily inspired by lean2md.
  10. Commit fbadcf5 builds on the recent leanprover/lean4:v4.9.0-rc2
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem