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 df255e2 builds on the recent leanprover/lean4:v4.15.0-rc1
    mathlib
    The math library of Lean 4
  2. Commit 1c84b5b builds on the recent leanprover/lean4:v4.15.0-rc1
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  3. Commit 8216cd9 builds on the recent leanprover/lean4:v4.15.0-rc1
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  4. Commit 466e162 builds on the recent leanprover/lean4:v4.15.0-rc1
    scilean
    Scientific computing in Lean 4
  5. Commit 8325355 builds on the recent leanprover/lean4:v4.15.0-rc1
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  6. Commit 5fb74b7 builds on the recent leanprover/lean4:v4.14.0-rc3
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  7. Commit f007bfe builds on the recent leanprover/lean4:v4.15.0-rc1
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  8. Commit 59e4e66 builds on the recent leanprover/lean4:v4.15.0-rc1
    lean4-metaprogramming-book
  9. Commit a4a08d9 builds on the recent leanprover/lean4:v4.15.0-rc1
    aesop
    White-box automation for Lean 4
  10. Commit 80f5638 builds on the recent leanprover/lean4:v4.15.0-rc1
    ntptutorial
    Tutorial on neural theorem proving

Newly Created

  1. Commit 415892f builds on the recent leanprover/lean4:v4.15.0-rc1
    vqc_in_lean
    Lean 4 port of the Verified Quantum Computing. Developed as a personal learning project to deepen understanding of quantum computing concepts and formal verification.
  2. Commit e7147ca builds on the recent leanprover/lean4:v4.15.0-rc1
    NodeGraph
  3. Commit 854b051 builds on the recent leanprover/lean4:v4.15.0-rc1
    partial-combinatory-algebras
    A Lean 4 formalization of partial combinatory algebras.
  4. Commit 2470c19 builds on the recent leanprover/lean4:v4.15.0-rc1
    CodeProofTheArena
    Lean coding problem solving challenge website with proof verification
  5. Commit 9f3241a builds on the recent leanprover/lean4:v4.15.0-rc1
    remco-mul
  6. Commit 4eb38e1 builds on the recent leanprover/lean4:v4.15.0-rc1
    order-pq
    Lean formalisation of the classification of the groups of order `p * q` where `p` and `q` are prime numbers.
  7. Commit 656070c builds on the recent leanprover/lean4:v4.15.0-rc1
    borel_det
  8. Commit 30ea6c4 fails to build on leanprover/lean4:v4.15.0-rc1
    verso-manual
    「The Lean Language Reference」の日本語訳(作業中)
  9. Commit 8e5cb8d builds on the recent leanprover/lean4:v4.15.0-rc1
    plausible
  10. Commit 8e24b93 builds on the old leanprover/lean4:v4.13.0-rc4
    FMCn_Lean
    Repositório destinado às práticas de Lean4 da Monitoria de FMCn.

Recently Updated

  1. Commit df255e2 builds on the recent leanprover/lean4:v4.15.0-rc1
    mathlib
    The math library of Lean 4
  2. Commit 22b918e builds on the recent leanprover/lean4:v4.15.0-rc1
    verbose
    Natural language tactics to teach mathematics using Lean 4
  3. Commit f007bfe builds on the recent leanprover/lean4:v4.15.0-rc1
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  4. Commit 84ad8f7 builds on the recent leanprover/lean4:v4.15.0-rc1
    aegis
    Verify Cairo contracts in Lean 4
  5. Commit 98d13bc builds on the recent leanprover/lean4:v4.15.0-rc1
    egg
    A (WIP) equality saturation tactic for Lean based on egg.
  6. Commit e898801 builds on the recent leanprover/lean4:v4.15.0-rc1
    Lean by Example
    プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。
  7. Commit 5fb74b7 builds on the recent leanprover/lean4:v4.14.0-rc3
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  8. Commit e1d9b71 builds on the recent leanprover/lean4:v4.15.0-rc1
    compfiles
    Catalog Of Math Problems Formalized In Lean
  9. Commit 0d7e8b6 builds on the recent leanprover/lean4:v4.15.0-rc1
    mdgen
    Tool to generate markdown files from lean files.
  10. Commit 3a42110 builds on the recent leanprover/lean4:v4.15.0-rc1
    Seymour
    This project is about formally verifying Seymour's decomposition theorem for regular matroids.