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

A collection of formalized statements of conjectures in Lean.

Converts floating point numbers to decimal strings

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)

Formal verification of the Riemann hypothesis up to bounded height by Lean's kernel, reaching height 10⁸

A tiny, verifiable agent library in Lean 4 that compiles to C

Lean 4 proof that the Jacobian conjecture in dimension 2n implies the Poisson conjecture in dimension n, Formal Conjectures' math/0608009 statement (Adjamagbo and van den Essen, Theorem 7)

∃ℝ ⊆ PSPACE formalized in Lean

Lean 4 proof that an AME(12,5) state exists, against Formal Conjectures' Open Quantum Problem 35, via a general graph-state criterion

XML 1.0 parsing semantics in Lean 4, with a resumable streaming core and a bounded differential fixture against libexpat.

Neumann cosine series on [0,L] and the discrete Neumann Laplacian in Lean 4 and Mathlib

The Lean Computer Science Library (CSLib)

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

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

Condensed & experimental proof systems for zk/fhe and semantics for agent coordination

A verifier for automated and interactive proofs about transition systems.

The math library of Lean 4

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

Formal prime certificates in Lean 4

Epistemic protocols for Claude Code — structure human-AI interaction quality at every decision point - https://epistemic-protocols.com

Lean specification of neural architectures with verified GPU codegen.