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

No results found

Latest Lean Stable:

leanprover/lean4:v4.21.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 958ad8b builds on the recent leanprover/lean4:v4.22.0-rc3
    mathlib
    The math library of Lean 4
  2. Commit 7714b4f builds on the recent leanprover/lean4:v4.22.0-rc3
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  3. Commit 3d91ad1 builds on the recent leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  4. Commit 353bd9c builds on the old leanprover/lean4:v4.17.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  5. Commit abe9a60 builds on the recent leanprover/lean4:v4.22.0-rc3
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  6. Commit c5a3e62 builds on the recent leanprover/lean4:v4.22.0-rc3
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  7. Commit 53f112d builds on the old leanprover/lean4:v4.15.0-rc1
    scilean
    Scientific computing in Lean 4
  8. Commit 5490062 builds on the recent leanprover/lean4:v4.20.1
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  9. Commit 82fd0cf builds on the recent leanprover/lean4:v4.22.0-rc3
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  10. Commit 7f3673d builds on the recent leanprover/lean4:v4.21.0
    PhysLean
    A project to digitalise results from physics into Lean.
All most popular

Newly Created

  1. Commit abdd5f4 builds on the recent leanprover/lean4:v4.22.0-rc3
    Numbers
    An introduction to numbers
  2. Commit f07cd5d builds on the recent leanprover/lean4:v4.22.0-rc3
    cslib
    A Lean library for Computer Science
  3. Commit 229da0f builds on the recent leanprover/lean4:v4.21.0
    goose
    GOOSE in Lean4
  4. Commit a2d4eab fails to build on leanprover/lean4:v4.22.0-rc3
    tactic-programming-beginner-guide
    Beginner's guide to Tactic Programming in Lean
  5. Commit ff89a04 builds on the recent leanprover/lean4:v4.22.0-rc3
    haskell-spec
    Formal specification of the Haskell Language Report
  6. Commit 3d91ad1 builds on the recent leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  7. Commit 3c0efe0 builds on the old leanprover/lean4:v4.19.0
    Lie
    A classification theorem in Lean of solvable Lie algebras of dimension zero to three
  8. Commit 312192d builds on the old leanprover/lean4-pr-releases:pr-release-8003
    mini-redis
    An implementation of mini-redis in Lean 4
  9. Commit 7351fae builds on the old leanprover/lean4:v4.18.0
    verina
    Verina (Verifiable Code Generation Arena) is a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions.
  10. Commit 279121f builds on the recent leanprover/lean4:v4.22.0-rc3
    SemicircleLaw
    Formalization of Wigner's Semicircle Law in Lean
All newly created

Recently Updated

  1. Commit 375127b builds on the recent leanprover/lean4:v4.22.0-rc3
    CombinatorialGames
    Combinatorial game library in Lean 4
  2. Commit 9880950 builds on the recent leanprover/lean4:v4.20.1
    TensorLib
    A verified tensor library in Lean
  3. Commit 3d91ad1 builds on the recent leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  4. Commit a275f35 builds on the recent leanprover/lean4:v4.20.1
    Clean
    Lean circuit DSL
  5. Commit 64a6adb builds on the old leanprover/lean4:v4.19.0
    KLR
    A formalization of ML kernel languages
  6. Commit d4e17a4 builds on the old leanprover/lean4:v4.18.0
    ix
    a zero-knowledge proof-carrying code platform for Lean 4
  7. Commit d5b5f18 builds on the recent leanprover/lean4:v4.22.0-rc2
    carleson
    A formalized proof of Carleson's theorem in Lean
  8. Commit 353bd9c builds on the old leanprover/lean4:v4.17.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  9. Commit a62ecd0 builds on the recent leanprover/lean4:v4.22.0-rc3
    aesop
    White-box automation for Lean 4
  10. Commit 958ad8b builds on the recent leanprover/lean4:v4.22.0-rc3
    mathlib
    The math library of Lean 4
All recently updated