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

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

The Lean Computer Science Library (CSLib)

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

Development monorepo for Hex: verified computational algebra in Lean 4 (polynomial factoring, LLL, and friends). Released aggregate: https://github.com/leanprover/hex

Formalization of complexity theory

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

The Lean Machine Learning Library

The math library of Lean 4

Verified graph rewriting (for dataflow circuits).

Formalization of IMO shortlist problems in Lean 4