Erdős Problem #751

Let \(G\) be a graph with chromatic number \(\chi(G)=4\). If \(m_1<m_2<\cdots\) are the lengths of the cycles in \(G\) then can \(\min(m_{i+1}-m_i)\) be arbitrarily large? The answer is no: Bondy and Vince [BoVi98] proved that every graph with minimum degree at least \(3\) has two cycles whose lengths differ by at most \(2\), and hence the same is true for every graph with chromatic number \(4\). `erdos_751.variants.finite` below carries the Lean proof. It assumes a finite vertex type, where this quantifies over any `V : Type`, and the two are joined by de Bruijn-Erdős: a graph that is not \(3\)-colourable has a finite subgraph that is not \(3\)-colourable, and cycles of that subgraph are cycles of the whole. Mathlib does not have de Bruijn-Erdős, so that step is not formalised here.