Exceptions to the ABC conjecture in Lean

Formalisation of the Kelley-Meka bound on Roth numbers

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.

Formalisation of some facts about event structures and reversibility

Formalization of exchangeability and three proofs of de Finetti's theorem in Lean 4, following Probabilistic Symmetries and Invariance Principles by Olav Kallenberg

Exponent pair database

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

Lean4 formalization with Artistotle of the arXiv paper 1906.11174

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