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.

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

The Lean Computer Science Library (CSLib)

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

⚗️ | Soma is a general-purpose dependently-typed functional programming language powered by Interaction Nets with a minimal runtime.

Lean 4 library characterizing the algebraic structure of metastability and consolidation in stochastic systems

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

Formalized Cryptography Proofs in Lean 4

Solving Competition Geometry Problems in Lean

A project to digitalise results from physics into Lean.

Formally Verified Arguments of Knowledge in Lean

Experiments on automation for Lean

LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.