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 a03ab30 builds on the recent leanprover/lean4:v4.22.0-rc3
    mathlib
    The math library of Lean 4
  2. Commit 7714b4f builds on the recent leanprover/lean4:v4.22.0-rc2
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  3. Commit 3d91ad1 builds on the recent leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  4. Commit 12904fc builds on the old leanprover/lean4:v4.17.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  5. Commit 9feced6 builds on the recent leanprover/lean4:v4.22.0-rc2
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  6. Commit 902b97d builds on the recent leanprover/lean4:v4.22.0-rc2
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  7. Commit 53f112d builds on the old leanprover/lean4:v4.15.0-rc1
    scilean
    Scientific computing in Lean 4
  8. Commit 4de9edc builds on the recent leanprover/lean4:v4.20.1
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  9. Commit 3cabaef builds on the recent leanprover/lean4:v4.22.0-rc3
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  10. Commit 79a3546 builds on the recent leanprover/lean4:v4.21.0
    PhysLean
    A project to digitalise results from physics into Lean.

Newly Created

  1. Commit 71a283a builds on the recent leanprover/lean4:v4.22.0-rc2
    Numbers
    An introduction to numbers
  2. Commit 3125b8a builds on the recent leanprover/lean4:v4.21.0-rc3
    cslib
    Lean library for Computer Science
  3. Commit a2d4eab fails to build on leanprover/lean4:v4.22.0-rc2
    tactic-programming-beginner-guide
    Beginner's guide to Tactic Programming in Lean
  4. Commit 1bdab83 builds on the recent leanprover/lean4:v4.22.0-rc2
    haskell-spec
    Formal specification of the Haskell Language Report
  5. Commit 3d91ad1 builds on the recent leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  6. Commit 3c0efe0 builds on the old leanprover/lean4:v4.19.0
    Lie
    A classification theorem in Lean of solvable Lie algebras of dimension zero to three
  7. Commit 312192d builds on the old leanprover/lean4-pr-releases:pr-release-8003
    mini-redis
    An implementation of mini-redis in Lean 4
  8. Commit 7351fae builds on the old leanprover/lean4:v4.18.0
    verina
    Verina (Verifiable Code Generation Arena) is a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions.
  9. Commit 6c99d80 builds on the recent leanprover/lean4:v4.22.0-rc2
    SemicircleLaw
    Formalization of Wigner's Semicircle Law in Lean
  10. Commit 7087b15 fails to build on leanprover/lean4:v4.22.0-rc2
    lie-classification
    Classification of Lie algebras in Lean

Recently Updated

  1. Commit a03ab30 builds on the recent leanprover/lean4:v4.22.0-rc3
    mathlib
    The math library of Lean 4
  2. Commit f5f81cd builds on the recent leanprover/lean4:v4.20.1
    Clean
    Lean circuit DSL
  3. Commit 13c9ccb builds on the old leanprover/lean4:v4.19.0-rc2
    Seymour
    This project is about formally verifying Seymour's decomposition theorem for regular matroids.
  4. Commit 4182d4d builds on the recent leanprover/lean4:v4.21.0
    Toric
    Formalisation of toric varieties in Lean 4
  5. Commit 1e08a0e fails to build on leanprover/lean4:v4.22.0-rc3
    verso-manual
    The Lean reference manual
  6. Commit 163ea67 builds on the recent leanprover/lean4:v4.22.0-rc2
    Lean by Example
    プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。
  7. Commit 559fd52 builds on the old leanprover/lean4:v4.18.0
    trestle
  8. Commit ae14d73 fails to build on leanprover/lean4:v4.22.0-rc2
    HopfieldNet
  9. Commit 7e8c7aa builds on the old leanprover/lean4:v4.16.0-rc1
    lean-regex
  10. Commit 3d91ad1 builds on the recent leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I