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.

An Universe for Mitar —— Classical Calculus

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

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.

Type-safe, deeply-embedded SQL query DSL for Lean 4 — LINQ-style pipelines and query! comprehensions compiling to parameterized SQL for SQLite, PostgreSQL, and SQL Server

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)

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

A collection of formalized statements of conjectures in Lean.

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

Lean 4 formalization of Leray-Hopf weak-solution existence for the incompressible Navier-Stokes equations on the periodic 3-torus and on R^3, via the Galerkin method. Two capstone theorems are proved kernel-only (no project axioms, no sorryAx); see README.md for the exact modeling scope and claims table.

Lean 4 formalization of Fluid Spacetime Omni-Theory (FSOT) 2.1 by Damian Arthur Palumbo

The Lean reference manual

Lean specification of neural architectures with verified IREE codegen.

verification toolchain for TypeScript (Tech Preview)