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 c46b5e4 builds on the recent leanprover/lean4:v4.13.0
    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
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  4. Commit 3df3ceb builds on the recent leanprover/lean4:v4.13.0
    scilean
    Scientific computing in Lean 4
  5. Commit 31a10a3 builds on the recent leanprover/lean4:v4.13.0
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  6. Commit 17ea847 builds on the recent leanprover/lean4:v4.13.0
    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 8ddda84 builds on the recent leanprover/lean4:v4.13.0-rc4
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  9. Commit 5f93489 builds on the recent leanprover/lean4:v4.13.0
    aesop
    White-box automation for Lean 4
  10. Commit 80f5638 builds on the recent leanprover/lean4:v4.13.0
    ntptutorial
    Tutorial on neural theorem proving

Newly Created

  1. Commit 46fb498 builds on the recent leanprover/lean4:v4.13.0
    remco-mul
  2. Commit 7173622 builds on the recent leanprover/lean4:v4.13.0
    order-pq
    Lean formalisation of the classification of the groups of order `p * q` where `p` and `q` are prime numbers.
  3. Commit 83e4f2e fails to build on leanprover/lean4:v4.13.0
    borel_det
  4. Commit d212dd7 builds on the recent leanprover/lean4:v4.13.0
    plausible
  5. Commit 8e24b93 builds on the recent leanprover/lean4:v4.13.0-rc4
    FMCn_Lean
    Repositório destinado às práticas de Lean4 da Monitoria de FMCn.
  6. Commit 5ae790f builds on the recent leanprover/lean4:v4.13.0-rc4
    Seminar
    Past contents of Lean Seminars in Bonn
  7. Commit c5d60b8 builds on the recent leanprover/lean4:v4.13.0
    LeanSudoku
    Playing Sudoku in the Lean 4 proof assistant
  8. Commit 42a29f0 builds on the recent leanprover/lean4:v4.13.0
    ExFormMathL4
  9. Commit c318c9f builds on the recent leanprover/lean4:v4.13.0
    LeanCourse
    Bonn Lean course for winter 24/25
  10. Commit 8ddda84 builds on the recent leanprover/lean4:v4.13.0-rc4
    equational_theories
    A project to map out the relations between different equational theories of Magmas.

Recently Updated

  1. Commit c46b5e4 builds on the recent leanprover/lean4:v4.13.0
    mathlib
    The math library of Lean 4
  2. Commit 8ddda84 builds on the recent leanprover/lean4:v4.13.0-rc4
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  3. Commit 0f09ff1 builds on the recent leanprover/lean4:v4.13.0-rc3
    testing_lower_bounds
    Information theory and hypothesis testing, in Lean
  4. Commit 15b5ff3 builds on the recent leanprover/lean4:v4.13.0
    UnicodeBasic
    Basic Unicode support for Lean 4
  5. Commit f3be290 builds on the recent leanprover/lean4:v4.13.0
    SSA
    A minimal development of SSA theory
  6. Commit a2b708e builds on the recent leanprover/lean4:v4.13.0-rc1
    ConNF
    A formal consistency proof of Quine's set theory New Foundations
  7. Commit 1f1b175 builds on the recent leanprover/lean4:v4.13.0-rc4
    foundation
    Lean4 Logic Formalization
  8. Commit 3d85ae5 builds on the recent leanprover/lean4:v4.13.0
    Calculemus2
    Proof exercises in Lean4 and Isabelle/HOL
  9. Commit 77448d6 builds on the recent leanprover/lean4:v4.13.0
    llmlean
    LLMs + Lean, on your laptop or in the cloud
  10. Commit 0664171 builds on the recent leanprover/lean4:v4.13.0
    Calculemus2_es
    Ejercicios de demostración con Lean4 e Isabelle/HOL.