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)

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

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

The "batteries included" extended library for the Lean programming language and theorem prover

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

Development repo for translating Software Foundations to Lean

The math library of Lean 4

Plutus Core, CEK Machine in Lean 4, tailored for Blaster usage

The Lean Computer Science Library (CSLib)

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