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 c8b35d4 builds on the recent leanprover/lean4:v4.32.0-rc1
    mathlib
    The math library of Lean 4
  2. Commit ef03205 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.32.0-rc1
    ryu
    Converts floating point numbers to decimal strings
  4. Commit 2458f73 builds on the recent leanprover/lean4:v4.32.0-rc1
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  5. Commit c4b3807 builds on the old leanprover/lean4:v4.27.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  6. Commit 941f909 builds on the recent leanprover/lean4:v4.32.0-rc1
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit e4693a5 builds on the recent leanprover/lean4:v4.31.0
    Physlib
    A project to digitalise results from physics into Lean.
  8. Commit 2772f42 builds on the recent leanprover/lean4:v4.32.0-rc1
    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 c85fb0b 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 99521b1 fails to build on leanprover/lean4:v4.32.0-rc1
    LogicQ
    An IR language for fault-tolerant quantum programming
  2. Commit d5708f1 fails to build on leanprover/lean4:v4.32.0-rc1
    lean-math-note
  3. Commit 72d5cef 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 6c115ef builds on the recent leanprover/lean4:v4.31.0
    solanalib
    ⚠️ Experimental | Prototype
  5. Commit 8ea4baa builds on the recent leanprover/lean4:v4.32.0-rc1
    KummerCriterion
    Proof of Kummer's criterion for regularity of a prime in Lean
  6. Commit c40ac65 fails to build on leanprover/lean4:v4.32.0-rc1
    FormalRV
    Formal resource verification of Shor's algorithm.
  7. Commit 2bdc834 fails to build on leanprover/lean4:v4.32.0-rc1
    EconCSLib
    AI-assisted Lean formalization for Economics and Computation research
  8. Commit 96ac193 builds on the recent leanprover/lean4:v4.32.0-rc1
    lean-redis
    full featured async redis client for lean 4
  9. Commit 21bc93d builds on the old leanprover/lean4:v4.28.0
    OrdvecFormalization
    Lean 4 formalization of finite Bayes-threshold optimality for OrdVec overlap models.
  10. Commit 2aede42 fails to build on leanprover/lean4:v4.32.0-rc1
    LiveLeanTriathlon
All newly created

Recently Updated

  1. Commit ae44721 builds on the recent leanprover/lean4:v4.32.0-rc1
    LeanMachineLearning
    The Lean Machine Learning Library
  2. Commit 0bdbeea builds on the recent leanprover/lean4:v4.32.0-rc1
    sparkle
    A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.
  3. Commit 7bc9f36 fails to build on leanprover/lean4:v4.32.0-rc1
    OpenGALib
  4. Commit 2bdc834 fails to build on leanprover/lean4:v4.32.0-rc1
    EconCSLib
    AI-assisted Lean formalization for Economics and Computation research
  5. Commit 3adec51 builds on the recent leanprover/lean4:v4.32.0-rc1
    foam
    geometry of hospitality
  6. Commit 72d5cef 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.
  7. Commit c8b35d4 builds on the recent leanprover/lean4:v4.32.0-rc1
    mathlib
    The math library of Lean 4
  8. Commit eead15f builds on the old leanprover/lean4:v4.30.0-rc2 after lake update
    EvmAsm
  9. Commit 7a823dd 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.
  10. Commit 5dee0f3 builds on the recent leanprover/lean4:v4.32.0-rc1 after lake update
    QuantumLogicalFramework
    quantum genesis constructive possibilist quantum logical synthesis
All recently updated