Reservoir

Verified efficient algorithms in Lean4.

A formalized proof of Carleson's theorem in Lean

Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexity

Central limit theorem in Lean

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

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

Fermat's Last Theorem for regular primes

Formalizing "Proofs from THE BOOK"

A project to digitalise results from high energy physics into Lean.

Formalization of IMO shortlist problems in Lean 4

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

Formalisation of the Kelley-Meka bound on Roth numbers

Formalisation of the Cambridge Part II and Part III courses Graph Theory, Combinatorics, Extremal and Probabilistic Combinatorics in Lean

WIP collections library for Lean 4

Bonn Lean course for winter 24/25

Armv8 Native Code Symbolic Simulator in Lean