A string graph is an intersection graph of finitely many continuous curves in the plane. Each graph vertex represents one curve, and two distinct vertices are adjacent precisely when their curves intersect (Davies et al. 2026).
Davies et al. (2026) gave a polynomial time algorithm that finds a balanced graph
separator of size 
in a string graph with 
edges. The separator leaves no connected
component containing more than two thirds of the original vertices.
Their argument repairs a gap in an earlier proof. Davies
et al. (2026) state that the main-body results were obtained without AI assistance.
They used Aristotle and GPT for Lean formalization. They separately credit GPT with
an initial stronger parameter bound in an appendix, not with discovering the main-body
separator theorem.
