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

No results found

Latest Lean Stable:

leanprover/lean4:v4.31.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 7d46b4c builds on the recent leanprover/lean4:v4.31.0
    mathlib
    The math library of Lean 4
  2. Commit 63fde17 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-rc2
    ryu
    Converts floating point numbers to decimal strings
  4. Commit 4ad50a8 builds on the old leanprover/lean4:v4.30.0
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  5. Commit c5234e6 builds on the old leanprover/lean4:v4.27.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  6. Commit c541ddc builds on the recent leanprover/lean4:v4.31.0-rc2
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit 851e49a builds on the old leanprover/lean4:v4.30.0
    Physlib
    A project to digitalise results from physics into Lean.
  8. Commit 70c5bf5 builds on the recent leanprover/lean4:v4.31.0
    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 0b6c326 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 6d8123b builds on the old leanprover/lean4:v4.30.0
    unsorry
    Autonomous agents proving theorems in Lean 4 - Seti@Home but for maths proofs using LLMs. Git is the queue, the kernel is the gate, no sorry survives.
  2. Commit 6a9e658 builds on the recent leanprover/lean4:v4.31.0-rc2
    KummerCriterion
    Proof of Kummer's criterion for regularity of a prime in Lean
  3. Commit bff75eb fails to build on leanprover/lean4:v4.30.0
    FormalRV
    Formal resource verification of Shor's algorithm.
  4. Commit e76411f builds on the old leanprover/lean4:v4.30.0
    lean-redis
    full feature async redis client for lean 4
  5. Commit 21bc93d builds on the old leanprover/lean4:v4.28.0
    OrdvecFormalization
    Lean 4 formalization of finite Bayes-threshold optimality for OrdVec overlap models.
  6. Commit 96e0da8 builds on the recent leanprover/lean4:v4.31.0-rc2
    Etheorem
  7. Commit 4b187f4 builds on the old leanprover/lean4:v4.29.0-rc6
    Quantum
    Lean formalization of the theory of quantum information and quantum computation
  8. Commit 22f70ed builds on the old leanprover/lean4:v4.28.0
    AgreeToDisagree
    Lean formalizations of the paper "We Can't Agree to Disagree, Formally: Aumann's Theorem and Assumption Accounting in Lean"
  9. Commit 453f4fe builds on the recent leanprover/lean4:v4.31.0-rc2
    lean_eff
    LeanEff is a small Lean 4 extensible-effects library
  10. Commit 587545a builds on the old leanprover/lean4:v4.30.0-rc2
    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.
All newly created

Recently Updated

  1. Commit 4a9f45a builds on the recent leanprover/lean4:v4.31.0
    Parser
    Parser Combinator Library for Lean 4
  2. Commit 68c8636 builds on the recent leanprover/lean4:v4.31.0
    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 6d8123b builds on the old leanprover/lean4:v4.30.0
    unsorry
    Autonomous agents proving theorems in Lean 4 - Seti@Home but for maths proofs using LLMs. Git is the queue, the kernel is the gate, no sorry survives.
  4. Commit 7b40c42 builds on the old leanprover/lean4:v4.29.1
    Strata
  5. Commit eead15f builds on the old leanprover/lean4:v4.30.0-rc2 after lake update
    EvmAsm
  6. Commit 224b03c builds on the old leanprover/lean4:v4.30.0-rc2
    Hex
    Verified computational algebra in Lean 4 — polynomial factoring, LLL, and friends
  7. Commit bd78196 builds on the old leanprover/lean4:v4.29.1
    ix
    a zero-knowledge proof-carrying code platform for Lean 4
  8. Commit 48aaad4 builds on the old leanprover/lean4:v4.30.0
    SphereEversion
    Formalization of the existence of sphere eversions
  9. Commit 70c5bf5 builds on the recent leanprover/lean4:v4.31.0
    cslib
    The Lean Computer Science Library (CSLib)
  10. Commit 7d46b4c builds on the recent leanprover/lean4:v4.31.0
    mathlib
    The math library of Lean 4
All recently updated