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.

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

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

Small, configurable proof search for inductive Lean goals

Lean certificates accompanying Navier-Stokes and Euler results

A Lean 4 formalization of the PCF bound 2^aleph_omega < aleph_(omega_4) under the strong-limit hypothesis.

A Lean 4 formalization of Chen's theorem (Goldbach 1+2).

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

The Lean Computer Science Library (CSLib)

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

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

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

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

A Lean 4 implementation of the Ethereum consensus specification for the Fulu, Gloas, Heze forks.

A collection of formalized statements of conjectures in Lean.