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

No results found

Latest Lean Stable:

leanprover/lean4:v4.30.0
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 eb15deb builds on the recent leanprover/lean4:v4.31.0-rc1
    mathlib
    The math library of Lean 4
  2. Commit e8d4832 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.31.0-rc1
    ryu
    Converts floating point numbers to decimal strings
  4. Commit 4ad50a8 builds on the recent leanprover/lean4:v4.30.0
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  5. Commit 71c4d02 builds on the old leanprover/lean4:v4.27.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  6. Commit f30ec5d builds on the recent leanprover/lean4:v4.31.0-rc1
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit f5242c9 builds on the recent leanprover/lean4:v4.30.0
    Physlib
    A project to digitalise results from physics into Lean.
  8. Commit 43f68e9 builds on the recent leanprover/lean4:v4.31.0-rc1
    cslib
    The Lean Computer Science Library (CSLib)
  9. Commit f4a4a54 builds on the old leanprover/lean4:v4.28.0
    mil
    The user home repository for the Mathematics in Lean tutorial.
  10. Commit c944afd builds on the old leanprover/lean4:v4.29.0-rc8
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
All most popular

Newly Created

  1. Commit 88e6dd6 fails to build on leanprover/lean4:v4.30.0
    KummerCriterion
    Proof of Kummer's criterion for regularity of a prime in Lean
  2. Commit bff75eb fails to build on leanprover/lean4:v4.30.0
    FormalRV
    Formal resource verification of Shor's algorithm.
  3. Commit c0394c1 builds on the recent leanprover/lean4:v4.30.0
    lean-redis
    full feature async redis client for lean 4
  4. Commit 21bc93d fails to build on leanprover/lean4:v4.31.0-rc1
    OrdvecFormalization
    Lean 4 formalization of finite Bayes-threshold optimality for OrdVec overlap models.
  5. Commit 05427f3 builds on the recent leanprover/lean4:v4.31.0-rc1
    Etheorem
  6. Commit 4b187f4 builds on the old leanprover/lean4:v4.29.0-rc6
    Quantum
    Lean formalization of the theory of quantum information and quantum computation
  7. Commit 22f70ed fails to build on leanprover/lean4:v4.31.0-rc1
    AgreeToDisagree
    Lean formalizations of the paper "We Can't Agree to Disagree, Formally: Aumann's Theorem and Assumption Accounting in Lean"
  8. Commit 453f4fe builds on the recent leanprover/lean4:v4.31.0-rc1
    lean_eff
    LeanEff is a small Lean 4 extensible-effects library
  9. Commit 108a139 fails to build on leanprover/lean4:v4.31.0-rc1
    formal-slt
    Zero-sorry Lean 4 library: finite-sample SLT bounds, sharp McDiarmid, PAC-Bayes Bernstein margin shell, and Dudley chaining. Standard Lean/Mathlib axioms only.
  10. Commit 0bad22a builds on the recent leanprover/lean4:v4.30.0
    reviser
    LCF checks theorem construction; reviser checks belief revision
All newly created

Recently Updated

  1. Commit eead15f builds on the recent leanprover/lean4:v4.30.0-rc2 after lake update
    EvmAsm
  2. Commit 0e16149 builds on the recent leanprover/lean4:v4.30.0 after lake update
    QuantumLogicalFramework
    quantum genesis constructive possibilist quantum logical synthesis
  3. Commit 71c4d02 builds on the old leanprover/lean4:v4.27.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  4. Commit f9f5733 builds on the recent leanprover/lean4:v4.30.0
    linglib
    A Lean 4 library for formal linguistics: semantics, syntax, pragmatics, morphology, phonology, and processing — formalized across competing frameworks for high interconnection density.
  5. Commit b11c3c2 builds on the old leanprover/lean4:v4.25.0-rc2
    Lean by Example
    プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。
  6. Commit b265a3b fails to build on leanprover/lean4:v4.31.0-rc1
    Vericoding
    tools and benchmarks for verified coding
  7. Commit 43f68e9 builds on the recent leanprover/lean4:v4.31.0-rc1
    cslib
    The Lean Computer Science Library (CSLib)
  8. Commit bd78196 builds on the recent leanprover/lean4:v4.29.1
    ix
    a zero-knowledge proof-carrying code platform for Lean 4
  9. 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.
  10. Commit eb15deb builds on the recent leanprover/lean4:v4.31.0-rc1
    mathlib
    The math library of Lean 4
All recently updated