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

A collection of formalized statements of conjectures in Lean.

Lean circuit DSL

Lean 4 port of Iris, a higher-order concurrent separation logic framework

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

Formally Verified Arguments of Knowledge in Lean

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

Lean documentation authoring tool

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