← All papers
Formalising Szemerédi's Regularity Lemma in Lean
cs.LO
Aug 1, 2022 · v1
TL;DR
Formalizes Szemerédi's Regularity Lemma in Lean using mathlib's graph theory library.
Abstract
This paper presents the first formalization of Szemerédi's Regularity Lemma in the Lean theorem prover using mathlib. The Regularity Lemma is a fundamental result in combinatorics stating that every sufficiently large graph can be partitioned into a bounded number of parts such that edges between most pairs of parts behave quasi-randomly. The formalization required developing supporting infrastructure for graph theory and energy arguments in mathlib.
Problem
Szemeredi's Regularity Lemma, a fundamental result in combinatorics stating that large graphs can be partitioned into boundedly many parts with quasi-random edge distribution between most pairs, had not been formally verified in a proof assistant.
Approach
The paper presents the first formalization of Szemeredi's Regularity Lemma in the Lean theorem prover using mathlib. The formalization required developing supporting infrastructure for graph theory and energy arguments within the mathlib library.
Results
The Regularity Lemma is fully formalized and machine-checked in Lean, contributing new graph theory infrastructure to mathlib.