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.

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

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

Kernel-checked theorem generalization for Lean

An Universe for Mitar —— Classical Calculus

Verified proof-geometry IR experiments for AI-guided theorem proving in Lean 4

Descriptive complexity in Lean 4: machine-model-free NP-completeness via first-order reductions, and the polynomial hierarchy via second-order alternation

The math library of Lean 4

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

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

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

LLMs as Copilots for Theorem Proving in Lean

LLMs + Lean, on your laptop or in the cloud

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

Lean specification of neural architectures with verified GPU codegen.