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

No results found

Latest Lean Stable:

leanprover/lean4:v4.25.2
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 57ecfb9 builds on the recent leanprover/lean4:v4.26.0-rc2
    mathlib
    The math library of Lean 4
  2. Commit 3d91ad1 builds on the old leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  3. Commit 6cd705a builds on the recent leanprover/lean4:v4.26.0-rc2 after lake update
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  4. Commit e2da58b builds on the recent leanprover/lean4:v4.25.2 after lake update
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  5. Commit 225623c builds on the old leanprover/lean4:v4.22.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  6. Commit d4e039c builds on the recent leanprover/lean4:v4.25.0-rc2
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  7. Commit 4de9edc builds on the old leanprover/lean4:v4.20.1
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  8. Commit 2bf0e10 builds on the old leanprover/lean4:v4.21.0
    mil
    The user home repository for the Mathematics in Lean tutorial.
  9. Commit 53f112d builds on the old leanprover/lean4:v4.15.0-rc1
    scilean
    Scientific computing in Lean 4
  10. Commit 745bdd6 builds on the recent leanprover/lean4:v4.25.2 after lake update
    PhysLean
    A project to digitalise results from physics into Lean.
All most popular

Newly Created

  1. Commit 0dbb921 builds on the recent leanprover/lean4:v4.25.2 after lake update
    Putnam
  2. Commit 4357969 builds on the recent leanprover/lean4:v4.25.2 after lake update
    clap
    Implementation of the Clap language for ZK Circuits in the Lean proof-assistant
  3. Commit 226aa7d builds on the recent leanprover/lean4:v4.26.0-rc2 after lake update
    VerifiedGPU
  4. Commit 63b965c builds on the recent leanprover/lean4:v4.26.0-rc2
    bottcher
    Verified computation of the Mandelbrot set Böttcher series
  5. Commit 59fc327 builds on the recent leanprover/lean4:v4.25.1
    ZFLean
    A practical framework for set-theoretical development in Lean
  6. Commit 3da61e6 builds on the old leanprover/lean4:v4.24.0
    Curve25519Dalek
    Verifying curve25519-dalek using Lean
  7. Commit 5bd21e6 builds on the old leanprover/lean4:v4.24.0-rc1
    mathmatic_in_elementary_number_th
    IMO题目的形式化2个题
  8. Commit 351c9de builds on the recent leanprover/lean4:v4.26.0-rc2 after lake update
    category-theory-in-context-lean
    Lean Companion to the Category Theory in Context textbook by Emily Riehl
  9. Commit 432c987 builds on the recent leanprover/lean4:v4.25.2 after lake update
    probability
  10. Commit 878bf2d builds on the recent leanprover/lean4:v4.25.1 after lake update
    RangeSetBlaze
All newly created

Recently Updated

  1. Commit 2f7e846 builds on the recent leanprover/lean4:v4.25.0 after lake update
    Foundation
    Formalization of Mathematical Logic
  2. Commit 57ecfb9 builds on the recent leanprover/lean4:v4.26.0-rc2
    mathlib
    The math library of Lean 4
  3. Commit 30cfb22 builds on the recent leanprover/lean4:v4.26.0-rc2
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  4. Commit 3d91ad1 builds on the old leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  5. Commit c2b4e27 builds on the recent leanprover/lean4:v4.26.0-rc2 after lake update
    Project
    A template for blueprint-driven formalization projects in Lean.
  6. Commit b11c3c2 builds on the recent leanprover/lean4:v4.25.0-rc2
    Lean by Example
    プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。
  7. Commit af1b423 builds on the old leanprover/lean4:v4.22.0
    glimpseOfLean
    An introduction to theorem proving in Lean for the impatient.
  8. Commit 1640518 builds on the recent leanprover/lean4:v4.26.0-rc2
    cslib
    The Lean Computer Science Library (CSLib)
  9. Commit 942b49e builds on the old leanprover/lean4:v4.23.0-rc2
    plonky3-example
    A framework for extracting and formally verifying constraint systems from the Plonky3 zkDSL in Lean.
  10. Commit 9130275 builds on the old leanprover/lean4:v4.24.0-rc1
    CombinatorialGames
    Combinatorial game library in Lean 4
All recently updated