Reservoir

Verified efficient algorithms in Lean4.

repository for the collaborative formalization seminar in Analysis in Bonn

Formalization of communication complexity in Lean

A formal consistency proof of Quine's set theory New Foundations

Document Generator for Lean 4

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

Exponent pair database

Fermat's Last Theorem for regular primes

Formalizing "Proofs from THE BOOK"

Formalization of Gröbner basis theory in Lean4 (WIP)

Basic HTTP definitions and parsing for Lean

A blueprint for a formalization of infinity-cosmos theory in Lean.

Formalization of Iwasawa Theory in LꓱꓯN (tentative)

libgccjit bindings for Lean4