Verified efficient algorithms in Lean4.

Formally Verified Arguments of Knowledge in Lean

A formalized proof of Artin-Wedderburn theorem in Lean4

Proof of concept for generating a blueprint directly from Lean source.

repository for the collaborative formalization seminar in Analysis in Bonn

Github repository for the 2025 Clay Summer School on Formalizing Class Field Theory

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

A project to formalize Fisher-Tippett-Gnedenko theorem (default project of course MS-EV0029)

Fermat's Last Theorem for regular primes

Formalizing "Proofs from THE BOOK"

Formalization of Mathematical Logic

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