Graph Separator

A graph separator is a set of vertices whose deletion separates a graph into smaller connected components. A balanced separator of an -vertex graph is a set whose deletion leaves no connected component with more than vertices. For a string graph with edges, a balanced separator of size can be found in polynomial time (Davies et al. 2026).

Conroy et al. (2026, Theorem 1) proved that every finite simple graph with vertices and no complete graph as a graph minor, for an integer , has a set of at most vertices whose deletion leaves every connected component with at most vertices. The explicit constant 16 therefore uses balance rather than the convention above. Repeated application inside the unique oversized connected component gives a -balanced separator of size , where denotes big-O notation. Conroy et al. (2026) attribute the technical ideas to GPT-6 Astra and simplifications to Claude Opus 5.5. The authors checked the argument and the principal statements of an AI-produced Lean formalization.