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.

Polylogarithm Problem Set.

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

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

Autoformalization of Baek's solution to the moving sofa problem: the Gerver sofa is optimal

Finite-dimensional copulas, dependence orders, and rank correlations in Lean 4

Lean 4 proof that Naslund's Conjecture 13 fails at q = 3: square-difference-free subsets of F_3[T] past 3^(3n/4)

Lean proofs of constructive binary X-ray families, counting bounds, and an extension theorem

Formal Verification Of Jolt zk-VM

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 Lean 4 library for formal linguistics: semantics, syntax, pragmatics, morphology, phonology, and processing — formalized across competing frameworks for high interconnection density.

The math library of Lean 4

The Lean Computer Science Library (CSLib)

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

A project to digitalise results from physics into Lean.

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

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

The "batteries included" extended library for the Lean programming language and theorem prover