Exceptions to the ABC conjecture in Lean

This is the repository for algorithm design.

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

A project to map out the relations between different equational theories of Magmas.

Formalization of Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture (companion to mathlib4 branch kim/erdos-unit-distance)

Independent comparator verification: the uniform-constant Erdős unit-distance conjecture is false (Alpöge 2026, formalized)

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