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 bc87839 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 c3c14d4 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 daf1ed9 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 7246ae1 builds on the old leanprover/lean4:v4.7.0
    lean4-metaprogramming-book
  7. Commit 3ab2c72 builds on the recent leanprover/lean4:v4.13.0-rc1
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  8. Commit b20a886 builds on the recent leanprover/lean4:v4.13.0-rc3
    aesop
    White-box automation for Lean 4
  9. Commit 80f5638 builds on the recent leanprover/lean4:v4.13.0-rc3
    ntptutorial
    Tutorial on neural theorem proving
  10. Commit 1aca48a builds on the recent leanprover/lean4:v4.13.0-rc1
    PFR
    Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)

Newly Created

  1. Commit b73afda builds on the recent leanprover/lean4:v4.13.0-rc3
    ExFormMathL4
  2. Commit e7b028a 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.
  3. Commit d1d3854 builds on the recent leanprover/lean4:v4.13.0-rc3
    TensorLib
    A verified tensor library in Lean
  4. Commit e9e1de6 builds on the recent leanprover/lean4:v4.13.0-rc3
    NewProject
  5. Commit 16cd688 builds on the recent leanprover/lean4:v4.13.0-rc3
    CommComp
    Formalization of communication complexity in Lean
  6. Commit 95d4f48 fails to build on leanprover/lean4:v4.13.0-rc3
    rubik
    Lean 4 formalization of Rubik's cubes
  7. Commit 1020b88 builds on the recent leanprover/lean4:v4.13.0-rc3
    MetaExamples
    Examples using MetaProgramming for writing tactics etc.
  8. Commit a8e927a builds on the old leanprover/lean4:v4.11.0-rc2
    tutorial
    Aeneas tutorial for ICFP
  9. Commit 3d6d72f builds on the recent leanprover/lean4:v4.13.0-rc3
    sadol
    Symbolic and Automatic Differentiation of Languages in Lean
  10. Commit 3ec2fa0 builds on the recent leanprover/lean4:v4.13.0-rc3
    Calculemus2_es
    Ejercicios de demostraciĆ³n con Lean4 e Isabelle/HOL.

Recently Updated

  1. Commit e7b028a 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.
  2. Commit 4ae310f builds on the recent leanprover/lean4:v4.13.0-rc3
    Project
    Template for blueprint-driven formalization projects in Lean.
  3. Commit 91eb658 builds on the recent leanprover/lean4:v4.13.0-rc3
    InfinityCosmos
    A blueprint for a formalization of infinity-cosmos theory in Lean.
  4. Commit bc87839 builds on the recent leanprover/lean4:v4.13.0-rc3
    mathlib
    The math library of Lean 4
  5. Commit 3679aba builds on the recent leanprover/lean4:v4.13.0-rc3
    expdb
    Exponent pair database
  6. Commit 0ad8dee builds on the recent leanprover/lean4:v4.13.0-rc3
    smt
    Tactics for discharging Lean goals into SMT solvers.
  7. Commit d2e847c builds on the recent leanprover/lean4:v4.13.0-rc3
    miniF2F-lean4
    miniF2F dataset ported into Lean 4
  8. Commit 31d09b1 builds on the recent leanprover/lean4:v4.13.0-rc1
    FormalBook
    Formalizing "Proofs from THE BOOK"
  9. Commit c3c14d4 builds on the recent leanprover/lean4:v4.13.0-rc3
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  10. Commit 1aca48a builds on the recent leanprover/lean4:v4.13.0-rc1
    PFR
    Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)