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

The math library of Lean 4

Lean certificates accompanying Navier-Stokes and Euler results

A Lean companion to Analysis I

Converts floating point numbers to decimal strings

A collection of formalized statements of conjectures in Lean.

LLMs as Copilots for Theorem Proving in Lean

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

A project to digitalise results from physics into Lean.

The Lean Computer Science Library (CSLib)

Formally verified runtime analysis of evolutionary algorithms in Lean 4 and Mathlib, checked theorem by theorem against the literature.

Web user interfaces written in Lean 4, compiled to WebAssembly (Memory64), with a native Lean server for SSR

A proof of Erdős Problem #173.

λProlog inside Lean 4: write tactics, commands and proof search as logic programs, share types with Lean both ways, and get kernel-checked proofs.

Explicit persistent failure of Euclidean quartic sum-of-squares exactness, formalized in Lean.

Matrix multiplication over rings through integer coefficient schemes

A 7-vertex tournament whose Sperner capacity exceeds the order of its largest transitive subtournament (Lean 4, kernel-only)

A Lean 4 library for formal linguistics: semantics, syntax, pragmatics, morphology, phonology, and processing — formalized across competing frameworks for high interconnection density.

The Lean Computer Science Library (CSLib)

a zero-knowledge proof-carrying code protocol for Lean 4

A Lean 4 + Mathlib formalization of uncertified DAG consensus (Mysticeti-style): machine-checked safety, liveness from eventual DAG synchrony, and five further arcs

Human-controlled roadmaps for Tau Ceti, an AIs-welcome Lean library downstream of Mathlib.

Tensor-network theory, formalized in Lean 4: the fundamental theorem of matrix product states, canonical forms, parent Hamiltonians, matrix-product density operators, and projected entangled pair states, building on the QICLean quantum-information library

Local memory for Codex. Reuse work across chats without LLM calls to organize it.

Development monorepo for Hex: verified computational algebra in Lean 4 (polynomial factoring, LLL, and friends). Released aggregate: https://github.com/leanprover/hex

quantum genesis constructive possibilist quantum logical synthesis

Claude/Codex skill and local workflow layer for efficient interaction with Lean 4 and Monte-Carlo Tree Search.