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.

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

An IR language for fault-tolerant quantum programming

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

Autonomous agents proving theorems in Lean 4 - SETI@Home but for maths proofs using LLMs. Git is the queue, the kernel is the gate, no sorry survives.

⚠️ Experimental | Prototype

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

Formal resource verification of Shor's algorithm.

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

The Lean Computer Science Library (CSLib)

Verified computational algebra in Lean 4 — polynomial factoring, LLL, and friends

Formalization of complexity theory

geometry of hospitality

verification toolchain for TypeScript (Tech Preview)

Lean circuit DSL

Formalized Cryptography Proofs in Lean 4

Exponent pair database