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 fada3e8 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 21f7dea 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 ad3ba5f 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 dd04633 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 7789eca 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 39a5192 builds on the recent leanprover/lean4:v4.13.0-rc3
    LeanCourse
    Bonn Lean course for winter 24/25
  4. Commit 7789eca 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 fada3e8 builds on the recent leanprover/lean4:v4.13.0-rc3
    mathlib
    The math library of Lean 4
  2. Commit 7f0d4a0 builds on the recent leanprover/lean4:v4.13.0-rc3
    EulerProducts
    An attempt at formalizing facts on Euler products in Lean
  3. Commit 3518550 builds on the recent leanprover/lean4:v4.13.0-rc3
    testing_lower_bounds
    Information theory and hypothesis testing, in Lean
  4. Commit c0fe06c builds on the recent leanprover/lean4:v4.13.0-rc3
    maze
    maze game encoded in Lean 4 syntax
  5. Commit 39a5192 builds on the recent leanprover/lean4:v4.13.0-rc3
    LeanCourse
    Bonn Lean course for winter 24/25
  6. Commit 202c52e builds on the recent leanprover/lean4:v4.13.0-rc3
    SSA
    A minimal development of SSA theory
  7. Commit c783b7a builds on the recent leanprover/lean4:v4.13.0-rc3
    hep_lean
    A project to digitalise results from high energy physics into Lean.
  8. Commit a4a366d builds on the recent leanprover/lean4:v4.13.0-rc1
    carleson
    A formalized proof of Carleson's theorem in Lean
  9. Commit 364815b builds on the recent leanprover/lean4:v4.13.0-rc3
    Zklib
    A Library for Formally Verified Cryptographic Proof Systems
  10. Commit 5b8d60c builds on the recent leanprover/lean4:v4.13.0-rc3
    egg
    A (WIP) equality saturation tactic for Lean based on egg.