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.

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

Pure Lean 4 gRPC stack (HTTP/2 + HPACK + gRPC) on Std.Async

Kernel-checked theorem generalization for Lean

An Universe for Mitar —— Classical Calculus

Verified proof-geometry IR experiments for AI-guided theorem proving in Lean 4

Descriptive complexity in Lean 4: machine-model-free NP-completeness via first-order reductions, and the polynomial hierarchy via second-order alternation

Lean 4 and Mathlib formalization of nonuniform Berry–Esseen bounds and Bentkus's multivariate Gaussian approximation over convex sets.

A verified core of accounting mechanics in Lean 4, paired with curated accounting judgment in the Open Knowledge Format (OKF).

A Lean Library for Domain Theory

Write Python modules in Lean! (WIP)

Lean-specified zkTEE: measured guest execution, hashed receipts, lean-grpc APIs

The Feit–Thompson odd order theorem in Lean 4, with the finite group theory library it required — Hall, Fitting, Frobenius groups, transfer, ZJ, Dade isometry, coherence

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 4 formalization of the Fundamental Theorem of Matrix Product States (arXiv:2011.12127)

(Mirror) A Music formalization library and DSL in Lean 4

A project to digitalise results from physics into Lean.