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

No results found

Latest Lean Stable:

leanprover/lean4:v4.33.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 abec794 builds on the recent leanprover/lean4:v4.34.0-rc1
    mathlib
    The math library of Lean 4
  2. Commit 8f9e0fc 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-rc1
    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 9f5ee77 builds on the old leanprover/lean4:v4.27.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  6. Commit 071d16b builds on the recent leanprover/lean4:v4.34.0-rc1
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  7. Commit 476d92a builds on the recent leanprover/lean4:v4.33.0
    Physlib
    A project to digitalise results from physics into Lean.
  8. Commit 809bb39 builds on the recent leanprover/lean4:v4.34.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 54edcda 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 4e4c28d builds on the recent leanprover/lean4:v4.33.0-rc1
    LeanFrontier
    A Lean 4 library of machine-generated, kernel-verified mathematics.
  2. Commit d2230ee builds on the recent leanprover/lean4:v4.34.0-rc1
    sendov
  3. 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.
  4. Commit 4d305b9 builds on the recent leanprover/lean4:v4.32.1
    lean-tee
    Lean-specified zkTEE: measured guest execution, hashed receipts, lean-grpc APIs
  5. Commit 0887548 builds on the recent leanprover/lean4:v4.32.1
    lean-grpc
    Pure Lean 4 gRPC stack (HTTP/2 + HPACK + gRPC) on Std.Async
  6. Commit f53f842 builds on the recent leanprover/lean4:v4.32.1
    SumDiffProof
  7. Commit 07ed6f9 builds on the recent leanprover/lean4:v4.33.0-rc1
    AutoGeneralization
    Kernel-checked theorem generalization for Lean
  8. Commit a4ca5ad fails to build on leanprover/lean4:v4.32.1
    Calculus_21
    An Universe for Mitar —— Classical Calculus
  9. Commit f8a851a builds on the recent leanprover/lean4:v4.32.2
    proofnet-ir
    Verified proof-geometry IR experiments for AI-guided theorem proving in Lean 4
  10. Commit c789440 builds on the recent leanprover/lean4:v4.33.0-rc1
    descriptive-complexity
    Descriptive complexity in Lean 4: machine-model-free NP-completeness via first-order reductions, and the polynomial hierarchy via second-order alternation
All newly created

Recently Updated

  1. Commit 365531d builds on the recent leanprover/lean4:v4.34.0-rc1
    TauCeti
    An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics
  2. Commit bd78196 builds on the old leanprover/lean4:v4.29.1
    ix
    a zero-knowledge proof-carrying code platform for Lean 4
  3. Commit 7c00469 builds on the recent leanprover/lean4:v4.33.0
    linglib
    A Lean 4 library for formal linguistics: semantics, syntax, pragmatics, morphology, phonology, and processing — formalized across competing frameworks for high interconnection density.
  4. Commit ed29cc9 builds on the recent leanprover/lean4:v4.34.0-rc1
    TNLean
    Lean 4 formalization of the Fundamental Theorem of Matrix Product States (arXiv:2011.12127)
  5. Commit 805cdb5 builds on the recent leanprover/lean4:v4.34.0-rc1
    verso
    Lean documentation authoring tool
  6. Commit eead15f builds on the old leanprover/lean4:v4.30.0-rc2 after lake update
    EvmAsm
  7. Commit 1507ca9 builds on the recent leanprover/lean4:v4.32.2
    formal-slt
    Machine-checked statistical learning theory in Lean 4: empirical-Bernstein and time-uniform PAC-Bayes, Markov risk, Rademacher/VC, and Dudley chaining.
  8. Commit abec794 builds on the recent leanprover/lean4:v4.34.0-rc1
    mathlib
    The math library of Lean 4
  9. Commit c1a92e7 builds on the old leanprover/lean4:v4.29.0
    clap
    Implementation of the Clap language for ZK Circuits in the Lean proof-assistant
  10. Commit d57c8e1 builds on the old leanprover/lean4:v4.31.0
    Arklib
    Formally Verified Arguments of Knowledge in Lean
All recently updated