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.

Stochastic Hybrid Systems core definitions formalized in Lean

The Seiberg-Witten solution of N=2 SU(2) super-Yang-Mills, formalized in Lean 4: physics as named postulates, machine-checked consequences, audited assumptions

Verified quantum computing in Lean 4 with FFI bridge to Apple Silicon (Metal 3). Full NISQ stack, dependent types, formal circuit verification, and mathematical translators to Hamiltonians for autonomous AI.

Leanstral's fork of SafeVerify, which we use for code agent training and as part of our evaluation stack.

Hax Lean library (automatically generated from cryspen/hax)

Formal verification of knowledge soundness for Generalized Bulletproofs

An IR language for fault-tolerant quantum programming

ZK recovery contract: design, audits, and prototyping (private)

Verified computational algebra in Lean 4: aggregator for the released hex libraries

A collection of formalized statements of conjectures in Lean.

Lean 4 formalization of the Fundamental Theorem of Matrix Product States (arXiv:2011.12127)

The math library of Lean 4

An attempt at formalizing the theory of heights in Lean

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

Formally Verified Float Implementation with lean4

The Lean Computer Science Library (CSLib)

Verified Bitcoin protocol components in Lean 4 — serialization, txids, and merkle commitments checked against real mainnet blocks.