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 1fef59c builds on the recent leanprover/lean4:v4.14.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 38f7775 builds on the recent leanprover/lean4:v4.13.0
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  4. Commit 7cbec80 builds on the recent leanprover/lean4:v4.13.0
    scilean
    Scientific computing in Lean 4
  5. Commit 76e9ebe builds on the recent leanprover/lean4:v4.14.0-rc1
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  6. Commit 1a17cd1 builds on the recent leanprover/lean4:v4.14.0-rc1
    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 0f3edc3 builds on the recent leanprover/lean4:v4.13.0
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  9. Commit 93bcfd7 builds on the recent leanprover/lean4:v4.14.0-rc1
    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 256986c builds on the recent leanprover/lean4:v4.13.0
    borel_det
  4. Commit 42dc02b builds on the recent leanprover/lean4:v4.14.0-rc1
    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 0c8aa3d builds on the recent leanprover/lean4:v4.13.0
    Seymour
  9. Commit 42a29f0 builds on the recent leanprover/lean4:v4.13.0
    ExFormMathL4
  10. Commit c318c9f builds on the recent leanprover/lean4:v4.13.0
    LeanCourse
    Bonn Lean course for winter 24/25

Recently Updated

  1. Commit 0f3edc3 builds on the recent leanprover/lean4:v4.13.0
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  2. Commit 1fef59c builds on the recent leanprover/lean4:v4.14.0-rc1
    mathlib
    The math library of Lean 4
  3. Commit 93bcfd7 builds on the recent leanprover/lean4:v4.14.0-rc1
    aesop
    White-box automation for Lean 4
  4. Commit 46fb498 builds on the recent leanprover/lean4:v4.13.0
    remco-mul
  5. Commit bcad3ee builds on the old leanprover/lean4:v4.11.0
    lost-pop-lean
    POP Memory Model in Lean
  6. Commit 3b8f5f1 builds on the recent leanprover/lean4:v4.13.0-rc3
    lnsym
    Armv8 Native Code Symbolic Simulator in Lean
  7. Commit 07da422 builds on the old leanprover/lean4:v4.5.0
    formalising-mathematics-2024
    Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.
  8. Commit 76e9ebe builds on the recent leanprover/lean4:v4.14.0-rc1
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  9. Commit 0f09ff1 builds on the recent leanprover/lean4:v4.13.0-rc3
    testing_lower_bounds
    Information theory and hypothesis testing, in Lean
  10. Commit d1d3854 builds on the recent leanprover/lean4:v4.13.0
    TensorLib
    A verified tensor library in Lean