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

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 7-vertex tournament whose Sperner capacity exceeds the order of its largest transitive subtournament (Lean 4, kernel-only)

Planar Euclidean dual-geodesic midpoint rigidity

The Complex Number Game, ported to Lean 4

Polylogarithm Problem Set.

The Escauriaza–Seregin–Šverák theorem, formalized in Lean 4

Lean proofs of the 43/80 upper bound for superpermutations, with explicit words on 8-13 symbols

Lean 4 SDK for Datastar: real-time hypermedia over server-sent events.

Two-fold Langford sequences exist exactly when 3l >= 2d - 1: a Lean 4 proof, with the m-fold counting bound attained for every m

Michael Spivak's Calculus formalized in Lean 4: every theorem and every problem of all 30 chapters and 9 appendices, in both the 3rd and 4th editions

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.

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

Machine-checked cryptographic proofs in Lean, built on Mathlib: oracle computations, probability semantics, program logic, and lattice- and hash-based schemes.

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 zero-knowledge proof-carrying code protocol for Lean 4

A minimal development of SSA theory

A Lean tactic for Canonical, a search procedure for terms in dependent type theory.

The math library of Lean 4