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.

Lean theorem proving interface which feels like pen-and-paper proofs.

Proof of Kummer's criterion for regularity of a prime in Lean

Formal resource verification of Shor's algorithm.

full feature async redis client for lean 4

Lean 4 formalization of finite Bayes-threshold optimality for OrdVec overlap models.

Lean formalization of the theory of quantum information and quantum computation

Lean formalizations of the paper "We Can't Agree to Disagree, Formally: Aumann's Theorem and Assumption Accounting in Lean"

LeanEff is a small Lean 4 extensible-effects library

Zero-sorry Lean 4 library: finite-sample SLT bounds, sharp McDiarmid, PAC-Bayes Bernstein margin shell, and Dudley chaining. Standard Lean/Mathlib axioms only.

LCF checks theorem construction; reviser checks belief revision

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

A collection of formalized statements of conjectures in Lean.

The Lean Computer Science Library (CSLib)

The math library of Lean 4

Proétale cohomology in Lean

Blueprint for the PNT+ Project

Github repository for the 2025 Clay Summer School on Formalizing Class Field Theory

Zero-sorry Lean 4 library: finite-sample SLT bounds, sharp McDiarmid, PAC-Bayes Bernstein margin shell, and Dudley chaining. Standard Lean/Mathlib axioms only.