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

The math library of Lean 4

A Lean companion to Analysis I

Converts floating point numbers to decimal strings

LLMs as Copilots for Theorem Proving in Lean

A collection of formalized statements of conjectures 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)

The user home repository for the Mathematics in Lean tutorial.

A project to map out the relations between different equational theories of Magmas.

A Lean 4 library of machine-generated, kernel-verified mathematics.

Lean 4 formalisation of the two examples in 'Uniform sheafy Tate rings that are not stably uniform' (Birkbeck-Torzewski), kernel-certified with leanprover/comparator

Write out the declaration graph of a Lean environment, statement dependencies kept apart from proof dependencies, so you can find what a theorem actually rests on.

Lean-specified zkTEE: measured guest execution, hashed receipts, lean-grpc APIs

Best-practice starter repository for Palomar submissions

Pure Lean 4 gRPC stack (HTTP/2 + HPACK + gRPC) on Std.Async

An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics

Development repo for translating Software Foundations to Lean

ASCI Summer Research Lean

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

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 collection of formalized statements of conjectures in Lean.

Neural network specification, execution, and verification in Lean 4.

Machine-checked statistical learning theory in Lean 4: empirical-Bernstein and time-uniform PAC-Bayes, Markov risk, Rademacher/VC, and Dudley chaining.