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 090e243 builds on the recent leanprover/lean4:v4.13.0-rc3
    mathlib
    The math library of Lean 4
  2. Commit 880f820 builds on the old leanprover/lean4:v4.11.0
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  3. Commit 992c4c8 builds on the recent leanprover/lean4:v4.13.0-rc3
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  4. Commit 145ab7f builds on the old leanprover/lean4:v4.11.0-rc2
    scilean
    Scientific computing in Lean 4
  5. Commit c521f01 builds on the recent leanprover/lean4:v4.13.0-rc3
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  6. Commit 77e137d builds on the recent leanprover/lean4:v4.13.0-rc3
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit a7fefe8 builds on the old leanprover/lean4:v4.7.0
    lean4-metaprogramming-book
  8. Commit b20a886 builds on the recent leanprover/lean4:v4.13.0-rc3
    aesop
    White-box automation for Lean 4
  9. Commit 88f806c builds on the recent leanprover/lean4:v4.13.0-rc3
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  10. Commit 80f5638 builds on the recent leanprover/lean4:v4.13.0-rc3
    ntptutorial
    Tutorial on neural theorem proving

Newly Created

  1. Commit 36cf0d0 builds on the recent leanprover/lean4:v4.13.0-rc3
    LeanSudoku
    Playing Sudoku in the Lean 4 proof assistant
  2. Commit 65faab7 builds on the recent leanprover/lean4:v4.13.0-rc3
    ExFormMathL4
  3. Commit a9062de builds on the recent leanprover/lean4:v4.13.0-rc3
    LeanCourse
    Bonn Lean course for winter 24/25
  4. Commit 88f806c builds on the recent leanprover/lean4:v4.13.0-rc3
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  5. Commit d1d3854 builds on the recent leanprover/lean4:v4.13.0-rc3
    TensorLib
    A verified tensor library in Lean
  6. Commit e9e1de6 builds on the recent leanprover/lean4:v4.13.0-rc3
    NewProject
  7. Commit 16cd688 builds on the recent leanprover/lean4:v4.13.0-rc3
    CommComp
    Formalization of communication complexity in Lean
  8. Commit 95d4f48 fails to build on leanprover/lean4:v4.13.0-rc3
    rubik
    Lean 4 formalization of Rubik's cubes
  9. Commit 1020b88 builds on the recent leanprover/lean4:v4.13.0-rc3
    MetaExamples
    Examples using MetaProgramming for writing tactics etc.
  10. Commit a8e927a builds on the old leanprover/lean4:v4.11.0-rc2
    tutorial
    Aeneas tutorial for ICFP

Recently Updated

  1. Commit adcdd8b builds on the recent leanprover/lean4:v4.13.0-rc3
    compfiles
    Catalog Of Math Problems Formalized In Lean
  2. Commit 090e243 builds on the recent leanprover/lean4:v4.13.0-rc3
    mathlib
    The math library of Lean 4
  3. Commit b424b1c builds on the old leanprover/lean4:v4.10.0 after lake update
    evmyul
    Executable formal model of the EVM and Yul in Lean 4.
  4. Commit 325da40 builds on the old leanprover/lean4:v4.9.0-rc3
    lean-training-data
  5. Commit f959e28 builds on the recent leanprover/lean4:v4.13.0-rc3
    GroundZero
    Ground Zero: Lean 4 HoTT Library
  6. Commit 32ec426 builds on the recent leanprover/lean4:v4.13.0-rc3
    LeanAPAP
    Formalisation of the Kelley-Meka bound on Roth numbers
  7. Commit c521f01 builds on the recent leanprover/lean4:v4.13.0-rc3
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  8. Commit 283abe4 builds on the recent leanprover/lean4:v4.13.0-rc3
    testing_lower_bounds
    Information theory and hypothesis testing, in Lean
  9. Commit 9362871 builds on the recent leanprover/lean4:v4.13.0-rc3
    jixia
    A static analysis tool for Lean 4.
  10. Commit 942f45d builds on the recent leanprover/lean4:v4.13.0-rc3
    BET
    Project for "Machine-Checked Mathematics" at the Lorentz Center