Reservoir

Verified efficient algorithms in Lean4.

repository for the collaborative formalization seminar in Analysis in Bonn

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

Fermat's Last Theorem for regular primes

Formalizing "Proofs from THE BOOK"

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

Bonn Lean course for winter 24/25

Armv8 Native Code Symbolic Simulator in Lean