This is Reservoir, the registry for all Lean packages and documentation.

No results found

Latest Lean Stable:

leanprover/lean4:v4.33.1
Get Started with Lean

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 52b284f builds on the recent leanprover/lean4:v4.34.0-rc2
    mathlib
    The math library of Lean 4
  2. Commit 2351317 builds on the old leanprover/lean4:v4.29.0-rc8
    Analysis
    A Lean companion to Analysis I
  3. Commit 4c0618b fails to build on leanprover/lean4:v4.34.0-rc2
    ryu
    Converts floating point numbers to decimal strings
  4. Commit 2458f73 builds on the recent leanprover/lean4:v4.34.0-rc1 after lake update
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  5. Commit 8323e87 builds on the recent leanprover/lean4:v4.33.1
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  6. Commit 8ec873a builds on the recent leanprover/lean4:v4.34.0-rc2
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit c17844a builds on the recent leanprover/lean4:v4.33.0
    Physlib
    A project to digitalise results from physics into Lean.
  8. Commit bba5e73 builds on the recent leanprover/lean4:v4.34.0-rc2
    cslib
    The Lean Computer Science Library (CSLib)
  9. Commit dd6d752 builds on the old leanprover/lean4:v4.30.0
    mil
    The user home repository for the Mathematics in Lean tutorial.
  10. Commit 88088fa builds on the old leanprover/lean4:v4.29.1
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
All most popular

Newly Created

  1. Commit 0296972 fails to build on leanprover/lean4:v4.34.0-rc2
    LocalComplexGeometry
    Foundational theorems in local complex-analytic geometry formalized in Lean 4
  2. Commit 32e7242 builds on the recent leanprover/lean4:v4.33.1 after lake update
    SphereCeti
  3. Commit f61ae6b builds on the recent leanprover/lean4:v4.33.1
    LeanFrontier
    A Lean 4 library of machine-generated, kernel-verified mathematics.
  4. Commit 2f45865 fails to build on leanprover/lean4:v4.33.1
    UniformSheafyTateDomains
    Lean 4 formalisation of the two examples in 'Uniform sheafy Tate rings that are not stably uniform' (Birkbeck-Torzewski), kernel-certified with leanprover/comparator
  5. Commit 1ddea92 builds on the recent leanprover/lean4:v4.34.0-rc2 after lake update
    sendov
  6. Commit cd064d6 builds on the recent leanprover/lean4:v4.34.0-rc2
    markdown
  7. Commit 0d2b3b5 builds on the recent leanprover/lean4:v4.32.1
    gonzalgo
    Write out the declaration graph of a Lean environment, statement dependencies kept apart from proof dependencies, so you can find what a theorem actually rests on.
  8. Commit 4d305b9 builds on the recent leanprover/lean4:v4.32.1
    lean-tee
    Lean-specified zkTEE: measured guest execution, hashed receipts, lean-grpc APIs
  9. Commit 128a6c5 fails to build on leanprover/lean4:v4.33.1
    PalomarTemplate
    Best-practice starter repository for Palomar submissions
  10. Commit 9779958 fails to build on leanprover/lean4:v4.33.1
    GroupApproximation
All newly created

Recently Updated

  1. Commit 4cac217 builds on the recent leanprover/lean4:v4.34.0-rc2
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  2. Commit e9dfda6 builds on the recent leanprover/lean4:v4.33.1
    linglib
    A Lean 4 library for formal linguistics: semantics, syntax, pragmatics, morphology, phonology, and processing — formalized across competing frameworks for high interconnection density.
  3. Commit d850eb2 builds on the recent leanprover/lean4:v4.34.0-rc1
    lean-pool
  4. Commit 52b284f builds on the recent leanprover/lean4:v4.34.0-rc2
    mathlib
    The math library of Lean 4
  5. Commit 9b9c059 builds on the recent leanprover/lean4:v4.34.0-rc2
    TauCeti
    An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics
  6. Commit 22dbd4e builds on the recent leanprover/lean4:v4.33.1
    Arklib
    Formally Verified Arguments of Knowledge in Lean
  7. Commit dc48e0c builds on the recent leanprover/lean4:v4.32.2
    lean4-mlir
    Lean specification of neural architectures with verified GPU codegen.
  8. Commit 4e7b392 builds on the old leanprover/lean4:v4.29.1
    Strata
  9. Commit f75e18d builds on the old leanprover/lean4:v4.25.0
    Blaster
    SMT-based reasoning core for Lean4
  10. Commit c17844a builds on the recent leanprover/lean4:v4.33.0
    Physlib
    A project to digitalise results from physics into Lean.
All recently updated