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.

Foundational theorems in local complex-analytic geometry formalized in Lean 4

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

Lean 4 formalisation of the two examples in 'Uniform sheafy Tate rings that are not stably uniform' (Birkbeck-Torzewski), kernel-certified with leanprover/comparator

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

Best-practice starter repository for Palomar submissions

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.

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

Comparator-based Lean formal mathematics eval

Development repo for translating Software Foundations to Lean

Formalization of complexity theory

Formalization of Mathematical Logic

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

a zero-knowledge proof-carrying code platform for Lean 4