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)

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

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

This repository hosts the SAIR Mathematics Distillation Challenge: Equational Theories Stage 2, providing Lean 4 problem sets, judging tools, and submission harnesses for generating machine-checkable proof certificates.

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

Library for formal language theory in Lean 4

Lean 4 formalization of De Giorgi-Nash-Moser theory

Formally verified machine learning in Lean 4.

LLM-assisted Lean specification of neural architectures with IREE codegen.

RFC 4648 Base64 encoding and decoding for Lean 4

A digital circuit verification library for Lean4

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.

The Lean Computer Science Library (CSLib)

LeanHammer is an automated reasoning tool for Lean that brings together multiple proof search and reconstruction techniques and combines them into one tool.

Library for formal language theory in Lean 4

The math library of Lean 4

Miscellaneous projects I am working on in Lean

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

A tool to auto-generate and render slides from Markdown comments in the Lean editor.