Fast Formal Proof of the Erdős–Szekeres Conjecture for Convex Polygons with at Most 6 Points

Abstract

A conjecture originally made by Klein and Szekeres in 1932 (now commonly known as “Erdős–Szekeres” or “Happy Ending” conjecture) claims that for every m≥ 3 , every set of 2 m-2 + 1 points in a general position (none three different points are collinear) contains a convex m-gon. The conjecture has been verified for m≤ 6. The case m= 6 was solved by Szekeres and Peters and required a huge computer enumeration that took “more than 3000 GHz hours”. In this paper we improve the solution in several directions. By changing the problem representation, by employing symmetry-breaking and by using modern SAT solvers, we reduce the proving time to around only a half of an hour on an ordinary PC computer (i.e., our proof requires only around 1 GHz hour). Also, we formalize the proof within the Isabelle/HOL proof assistant, making it significantly more reliable.