Strong edge-colouring via local flag algebras
Eoin Davey, Eoin Hurley, Rémi de Joannis de Verclos, Ross J. Kang, Jan Volec
math.CO
Jul 19, 2026 · v1
cs.DM
TL;DR
All four main theorems and Proposition 8.1 are formalised in Lean 4. Lean checks the rationalised flag-algebra SDP certificates, and an AI agent built some proofs directly in Lean.
Abstract
The strong chromatic index $χ'_s(G)$ is the smallest number of colours needed to colour the edges of a graph $G$ so that any two edges at distance at most $2$ receive different colours. Using the local flag algebra framework introduced in a companion paper, we prove $χ'_s(G) \leq 1.73\,Δ(G)^2$ for every graph $G$ of maximum degree $Δ(G)$, $χ'_s(G) \leq 1.6255\,Δ(G)^2$ for every bipartite $G$, and $χ'_s(G) \leq 1.6633\,Δ_A(G)\,Δ_B(G)$ for every bipartite $G$ of side maximum degrees $Δ_A(G), Δ_B(G)$ with rational $Δ_B(G)/Δ_A(G) \in (0, 1]$, provided $Δ(G)$, $Δ_A(G)$, $Δ_B(G)$ are sufficiently large. These three bounds make progress towards three established conjectures: those of Erdős-Nešetřil (1985) for general graphs, Faudree-Gyárfás-Schelp-Tuza (1989) for bipartite graphs, and Brualdi-Quinn Massey (1993) in the asymmetric bipartite setting. Additionally, for the random bipartite graph $G \sim G(n_A, n_B, p)$ at constant $p \in (0,1)$ and bounded aspect ratio $\max(n_A, n_B) = O(\min(n_A, n_B))$, we prove the Brualdi-Quinn Massey bound $χ'_s(G) \leq Δ_A(G)\,Δ_B(G)$ asymptotically almost surely.
Problem
The goal is to improve upper bounds on the strong chromatic index of graphs. This is progress toward the Erdős–Nešetřil, Faudree–Gyárfás–Schelp–Tuza, and Brualdi–Quinn Massey conjectures for general, bipartite, and asymmetric bipartite graphs.
Approach
The method uses local flag algebras, a variant of Razborov's flag algebras with densities normalised by maximum degree. This bounds the strong-neighbourhood density of L(G)^2, and the bound is fed into a sparse colouring lemma. Size-5 SDP certificates are generated by a Rust crate, solved numerically, rationalised, and verified in Lean 4. The random bipartite result and auxiliary propositions were proved in Lean with an agentic AI system under the authors' guidance.
Results
The bounds obtained are χ'_s ≤ 1.73Δ² for general graphs and ≤ 1.6255Δ² for bipartite graphs. For bipartite graphs with rational side-degree ratio the bound is ≤ 1.6633Δ_AΔ_B. The Brualdi–Quinn Massey bound holds a.a.s. for random bipartite graphs. All these results are formalised in Lean 4, with a public repository mapping each result to its Lean statement.
| Setting | Bound |
|---|
| General graphs | χ'_s ≤ 1.73 Δ² |
| Bipartite | χ'_s ≤ 1.6255 Δ² |
| Asymmetric bipartite (rational ratio) | χ'_s ≤ 1.6633 Δ_A Δ_B |
| Random bipartite G(n_A,n_B,p) | χ'_s ≤ Δ_A Δ_B a.a.s. |
Main bounds (Δ sufficiently large)
