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 f508fa4 builds on the recent leanprover/lean4:v4.34.0-rc2
    mathlib
    The math library of Lean 4
  2. Commit 245b2e1 builds on the old leanprover/lean4:v4.29.0-rc8
    Analysis
    A Lean companion to Analysis I
  3. Commit f9e8bc5 builds on the recent leanprover/lean4:v4.34.0-rc2
    NavierStokesAndEuler
    Lean certificates accompanying Navier-Stokes and Euler results
  4. Commit 4c0618b fails to build on leanprover/lean4:v4.34.0-rc2
    ryu
    Converts floating point numbers to decimal strings
  5. Commit 2458f73 builds on the recent leanprover/lean4:v4.34.0-rc1 after lake update
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  6. Commit 670c4e2 builds on the recent leanprover/lean4:v4.33.1
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  7. Commit 81d8bee builds on the recent leanprover/lean4:v4.34.0-rc2
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  8. Commit 8b2b237 builds on the recent leanprover/lean4:v4.33.0
    Physlib
    A project to digitalise results from physics into Lean.
  9. Commit ec95751 builds on the recent leanprover/lean4:v4.34.0-rc2
    cslib
    The Lean Computer Science Library (CSLib)
  10. Commit dd6d752 builds on the old leanprover/lean4:v4.30.0
    mil
    The user home repository for the Mathematics in Lean tutorial.
All most popular

Newly Created

  1. Commit f9e8bc5 builds on the recent leanprover/lean4:v4.34.0-rc2
    NavierStokesAndEuler
    Lean certificates accompanying Navier-Stokes and Euler results
  2. Commit a26427e builds on the old leanprover/lean4:v4.32.0-rc1
    kakeya
  3. Commit 9ecf082 builds on the old leanprover/lean4:v4.30.0
    pcfAlephOmega4
    A Lean 4 formalization of the PCF bound 2^aleph_omega < aleph_(omega_4) under the strong-limit hypothesis.
  4. Commit df1f3b3 builds on the recent leanprover/lean4:v4.33.0-rc1
    goldbach
    A Lean 4 formalization of Chen's theorem (Goldbach 1+2).
  5. Commit 82ffb75 builds on the old leanprover/lean4:v4.28.0
    Erdos548
    Lean 4 Erdős problem #548 (Erdős–Sós conjecture): proof, found by GPT-6 Astra in the FrontierMath Erdős benchmark; Palomar submission repository
  6. Commit ed6ab14 builds on the recent leanprover/lean4:v4.34.0-rc2
    dLean
  7. Commit 0296972 fails to build on leanprover/lean4:v4.34.0-rc2
    LocalComplexGeometry
    Foundational theorems in local complex-analytic geometry formalized in Lean 4
  8. Commit 6ac1d73 fails to build on leanprover/lean4:v4.34.0-rc2
    eggshell
    Local memory for Codex. Reuse work across chats without LLM calls to organize it.
  9. Commit 38f5a43 builds on the recent leanprover/lean4:v4.33.0
    langlib
    Esoteric Programming Languages, Formally
  10. Commit 4e79656 builds on the recent leanprover/lean4:v4.33.0
    FsFormal
    Palomar-ready Lean formalization of an improved Furstenberg-Sarkozy lower bound
All newly created

Recently Updated

  1. Commit 670c4e2 builds on the recent leanprover/lean4:v4.33.1
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  2. Commit 6e1e662 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 a5bdcff 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
  4. Commit 71b08c2 builds on the recent leanprover/lean4:v4.34.0-rc2
    Hex
    Development monorepo for Hex: verified computational algebra in Lean 4 (polynomial factoring, LLL, and friends). Released aggregate: https://github.com/leanprover/hex
  5. Commit 58eb097 builds on the recent leanprover/lean4:v4.33.1
    ix
    a zero-knowledge proof-carrying code protocol for Lean 4
  6. Commit 26f2840 builds on the recent leanprover/lean4:v4.34.0-rc2
    TauCetiRoadmap
    Human-controlled roadmaps for Tau Ceti, an AIs-welcome Lean library downstream of Mathlib.
  7. Commit f9e8bc5 builds on the recent leanprover/lean4:v4.34.0-rc2
    NavierStokesAndEuler
    Lean certificates accompanying Navier-Stokes and Euler results
  8. Commit a042dcd builds on the recent leanprover/lean4:v4.33.1
    VCVio
    Machine-checked cryptographic proofs in Lean, built on Mathlib: oracle computations, probability semantics, program logic, and lattice- and hash-based schemes.
  9. Commit 4c0618b fails to build on leanprover/lean4:v4.34.0-rc2
    ryu
    Converts floating point numbers to decimal strings
  10. Commit 988a1ab builds on the recent leanprover/lean4:v4.33.1
    PolyFun
    Lean 4 library for polynomial functors, interaction trees, and frameworks for modeling interactive and effectful protocols
All recently updated