Exceptions to the ABC conjecture in Lean

Formally Verified Arguments of Knowledge in Lean

A formalized proof of Artin-Wedderburn theorem in Lean4

repository for the collaborative formalization seminar in Analysis in Bonn

Construction of a Brownian Motion in Lean

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

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

Central limit theorem in Lean

Distributed Graph Algorithms in Lean

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)

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

Fermat's Last Theorem for regular primes

Formalizing "Proofs from THE BOOK"

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