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 b202b86 builds on the recent leanprover/lean4:v4.15.0-rc1
    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.15.0-rc1
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  4. Commit 1ddfae2 builds on the recent leanprover/lean4:v4.14.0-rc3
    scilean
    Scientific computing in Lean 4
  5. Commit 7be1a35 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.
  6. Commit f7c20d3 builds on the recent leanprover/lean4:v4.15.0-rc1
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit 74dffd1 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 3f28838 builds on the old leanprover/lean4:v4.7.0
    lean4-metaprogramming-book
  9. Commit 43bcb19 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 15d646d builds on the recent leanprover/lean4:v4.15.0-rc1
    partial-combinatory-algebras
    A Lean 4 formalization of partial combinatory algebras.
  2. Commit 2470c19 builds on the recent leanprover/lean4:v4.15.0-rc1
    CodeProofTheArena
    Lean coding problem solving challenge website with proof verification
  3. Commit 9f3241a builds on the recent leanprover/lean4:v4.15.0-rc1
    remco-mul
  4. 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.
  5. Commit d963baa builds on the recent leanprover/lean4:v4.14.0-rc3
    borel_det
  6. Commit dcae236 fails to build on leanprover/lean4:v4.15.0-rc1
    verso-manual
    「The Lean Language Reference」の日本語訳(作業中)
  7. Commit 8e5cb8d builds on the recent leanprover/lean4:v4.15.0-rc1
    plausible
  8. 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.
  9. Commit 5ae790f builds on the old leanprover/lean4:v4.13.0-rc4
    Seminar
    Past contents of Lean Seminars in Bonn
  10. Commit c5d60b8 builds on the recent leanprover/lean4:v4.15.0-rc1
    LeanSudoku
    Playing Sudoku in the Lean 4 proof assistant

Recently Updated

  1. Commit b202b86 builds on the recent leanprover/lean4:v4.15.0-rc1
    mathlib
    The math library of Lean 4
  2. Commit 9cb42e1 builds on the old leanprover/lean4:v4.13.0
    sampcert
    SampCert : Verified Differential Privacy
  3. Commit 588a32a builds on the recent leanprover/lean4:v4.15.0-rc1
    Lean by Example
    プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。
  4. Commit 8743a5c builds on the recent leanprover/lean4:v4.15.0-rc1
    pumping_cfg
  5. Commit dbb5545 fails to build on leanprover/lean4:v4.15.0-rc1
    verso-manual
  6. Commit 59b6839 builds on the recent leanprover/lean4:v4.15.0-rc1
    ConNF
    A formal consistency proof of Quine's set theory New Foundations
  7. Commit d9f20f5 builds on the old leanprover/lean4:nightly-2023-01-10
    yatima
    A zero-knowledge Lean4 compiler and kernel
  8. Commit dcae236 fails to build on leanprover/lean4:v4.15.0-rc1
    verso-manual
    「The Lean Language Reference」の日本語訳(作業中)
  9. Commit 8267c2a builds on the recent leanprover/lean4:v4.15.0-rc1
    SSA
    A minimal development of SSA theory
  10. Commit 1e87fd7 builds on the recent leanprover/lean4:v4.15.0-rc1
    tryAtEachStep
    Try a tactic at each step in a Lean proof.