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

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

A library for discovering truth: questions, computation, reusable proofs, and an open frontier.

Lean specification of neural architectures with verified GPU codegen.

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

The Lean Computer Science Library (CSLib)

Formal prime certificates in Lean 4

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

A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.

Combinatorial game library in Lean 4