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

Distributed Graph Algorithms in Lean

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

Proof of Kaplanski criterion for being a UFD in Lean4

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