Papers With

← All papers
First page of An explicit bound on the extremal function for complete graph minors

An explicit bound on the extremal function for complete graph minors

David R. Wood

math.CO Oct 29, 2026 · v1
formalization mathlib combinatorics
Read PDF arXiv abstract
TL;DR
The main theorem, including all numerical computations, is formally verified in Lean 4 with Mathlib, and the Lean files are provided as arXiv ancillary files.
Abstract
Kostochka and Thomason independently proved that every graph with density at least $β\,t\sqrt{\log t}$ has a $K_t$ minor, for some constant $β$. Thomason later proved that the least such density is $(0.319\ldots+o(1))\,t\sqrt{\log t}$. However, the $o(1)$ term in this formula is not explicit, so the formula gives no bound for any specific value of $t$. The goal of this paper is a bound of the form $β\,t\sqrt{\log t}$ that holds for every $t$, with $β$ small. We prove that, for every integer $t\geqslant2$, every graph with density at least $4.5\,t\sqrt{\log t}$ has a $K_t$ minor.
Problem

Thomason showed that the extremal density for K_t minors is (0.319...+o(1)) t√(log t). The o(1) term is not explicit, so the result gives no bound for any specific t. The goal is a bound β t√(log t) with small β that holds for every t ≥ 2.

Approach

The proof optimises the constants in Thomason's original argument. It uses two reductions (Mader-style minimal minors and density functions) and a core lemma that builds K_m minors in graphs where every vertex has few non-neighbours. Medium values of t (4 to 400) are handled by computer-certified density functions and admissible sequences. Claude Opus wrote the numeric scripts and the Lean 4/Mathlib formalisation, and the Lean kernel checks every computation.

Results

For every integer t ≥ 2, every graph with density at least 4.5 t√(log t) has a K_t minor. The full statement, kt_minor_45, is machine-checked in Lean 4 with Mathlib.