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.

Lean theorem proving interface which feels like pen-and-paper proofs.

The Lean Computer Science Library (CSLib)

A project to map out the relations between different equational theories of Magmas.

Cardano Ledger Api providing the necessary types and predicates to prove Plutus smart contracts with Blaster

Library for formal language theory in Lean 4

Formally verified machine learning in Lean 4.

Use Lean4 to build and train image recognition networks in MLIR.

Machine-verified proof (0 sorries, 2 axioms) that P ≠ NP via exponential circuit lower bounds for Hamiltonian Cycle. Lean 4 formalization with Mathlib. Proves SIZE(HAM_n) ≥ 2^{Ω(n)} using frontier analysis, switch blocks, cross-pattern mixing, recursive funnel magnification, continuation packets, rooted descent, and signature rigidity.

Algorithms and Complexity Library using the lightweight query combinator framework called "Prog"

Executable Hermite and Smith Normal Forms in Lean 4 over Euclidean Domains, with a PID bridge to mathlib.

literate programming for lean4

The math library of Lean 4

Verified Optimizing Compiler for Cryptographic Primitives

Use Lean4 to build and train image recognition networks in MLIR.

Semantic Versioning in Lean4

Converts floating point numbers to decimal strings

Formalized Cryptography Proofs in Lean 4

Plain-text declaration export for Lean 4

A formalization of ML kernel languages