Erdős #216 — the empty hexagon number g(6) (and non-existence for k≥7)

Statement

For $k\geq 3$, let $g(k)$ be the smallest integer (if it exists) such that any $g(k)$ points in $\mathbb{R}^2$ in general position (no three collinear) contain an empty convex $k$-gon — i.e. $k$ points forming a convex polygon with no other point of the set in its interior (also called a "$k$-hole"). Does $g(k)$ exist for every $k$? If so, estimate it.

This is a variant of the Erdős–Klein–Szekeres "happy ending" problem Erdős #107 — exact Erdős–Szekeres convex-polygon constant, which asks the analogous question *without* the emptiness restriction. (erdosproblems.com/216, citing [Er78c],[Er81],[Er82e],[Er83c],[Er97e].)

Facts

- Status on erdosproblems.com: DISPROVED — the question "does $g(k)$ exist for every $k$" is answered no in general (it fails at $k=7$), while for $k\le 6$ the numbers exist and (for $k\le 6$) are now all known exactly. - $g(3)=3$, $g(4)=5$ trivially/by the same argument as the happy-ending problem (Erdős). - $g(5)=10$: Harborth, "Konvexe Fünfecke in ebenen Punktmengen," Elem. Math. (1978) 116–118. - $g(6)$ exists: proved *independently* by Carlos M. Nicolás ("The Empty Hexagon Theorem," Discrete Comput. Geom. (2007) 389–397) and Tobias Gerken ("Empty convex hexagons in planar point sets," Discrete Comput. Geom. (2008) 239–272) — both submitted/circulated around 2006, closing a question open since Erdős posed it (~1978). Nicolás's route gave $h(6)\le g(25)$; Gerken's gave the much better $h(6)\le g(9)\le 1717$ (via Erdős–Szekeres $\mathrm{ES}(9)$); Valtr later gave a structurally simpler variant of Gerken's argument at the cost of a weaker bound ($f(15)$ instead of $f(9)$). - $g(k)$ does NOT exist for any $k\geq 7$: J. D. Horton, "Sets with no empty convex 7-gons," Canad. Math. Bull. (1983) 482–484 — an explicit recursive construction ("Horton sets") of arbitrarily large point sets in general position with no empty convex 7-gon at all; since a 7-hole-free set is automatically $k$-hole-free for all $k\ge7$, this simultaneously kills existence for every $k\ge 7$. To date every known 7-hole-avoiding construction is (a variant of) a Horton set. - Exact value $g(6)=30$: Marijn J. H. Heule and Manfred Scheucher, "Happy Ending: An Empty Hexagon in Every Set of 30 Points," TACAS 2024 (LNCS, 61–80), arXiv:2403.00737 — closed the gap between the best lower-bound construction (a 29-point hexagon-free set) and Gerken's upper bound via a massively parallel SAT search, giving the exact bound $h(6)=30$ (also written $g(6)=30$). Formally verified end-to-end in the Lean theorem prover by Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, and Marijn J. H. Heule, "Formal Verification of the Empty Hexagon Number," ITP 2024, arXiv:2403.17370. - Related OEIS sequence: A381776. This problem is also listed as #2 in the "Ramsey Theory" section of the UCSD Erdős-problems graphs collection (mathweb.ucsd.edu/~erdosproblems, per erdosproblems.com/216). - One-comment forum thread on erdosproblems.com/forum/discuss/216 points back to #107, confirming the two problems are treated as a linked pair by the site's own community.

Solution

Answer: $g(k)$ exists (is finite) exactly for $k\in\{3,4,5,6\}$, with $g(3)=3$, $g(4)=5$, $g(5)=10$, $g(6)=30$ (the last proved exactly only in 2024); for every $k\geq 7$, $g(k)$ does not exist — Horton's construction gives arbitrarily large empty-7-gon-free point sets. So the original "does $g(k)$ exist for all $k$" question is disproved, while the finite sub-case $k=6$ was fully pinned down.

The transferable technique — the problem was cracked in two structurally different stages, and both are reusable templates:

1. Existence (Nicolás 2007 / Gerken 2008) — reduce a "does it exist" geometry question to a Ramsey-type covering argument on convex layers or sub-configurations. Both proofs work by showing that *some* fixed, small convex configuration forces a 6-hole, then invoking the Erdős–Szekeres theorem Erdős #107 — exact Erdős–Szekeres convex-polygon constant (every sufficiently large point set contains a large convex polygon) to guarantee that configuration appears. Gerken's version: prove the purely local claim "every convex 9-gon (9 points already known to be in convex position) contains an empty hexagon among its points" — a finite, checkable structural fact — then plug in $\mathrm{ES}(9)$ to get a finite bound $g(9)\le\mathrm{ES}(9)=1717$ on the number of points needed. Nicolás's version instead works through the convex-layer structure of a point set (minimal convex subsets and their "children" under repeated convex-hull peeling), locating the hexagon by a case analysis over convex layers rather than a single flat convex polygon. The general lesson: *existence* proofs for Ramsey-type geometric extremal numbers can often be split into (a) a finite, purely combinatorial "local forcing lemma" about one fixed small structure, composed with (b) an existing black-box Ramsey/Erdős–Szekeres-type theorem that guarantees the structure appears — this decouples the hard finite geometry from the (already solved) infinitary pigeonhole step.

2. Exact value (Heule & Scheucher 2024) — turn the finite residual gap into a single SAT-solvable propositional formula, at the largest scale yet used for an open Erdős-type geometry question. After Gerken's proof pinned $h(6)\le1717$ (later improved by hand/computer to much smaller values, with a 29-point hexagon-free lower-bound construction already known), the exact value $h(6)=30$ was still an open finite gap. Heule and Scheucher encoded "there exists a 30-point set in general position, expressible via its order type (the combinatorial data of all point-triple orientations), with no empty convex hexagon" as a CNF formula $\varphi_n$ with $O(n^4)$ clauses, connecting propositional variables to point-triple orientations via known order-type/CC-system axioms. Proving $\varphi_{30}$ UNSAT (via a SAT solver, using an effective compact encoding plus a search-space-partitioning "cube-and-conquer"-style strategy achieving near-linear parallel speedup across thousands of cores, ~17,300 CPU-hours total) is a rigorous proof that no such 30-point set exists — combined with the known 29-point construction that does avoid an empty hexagon, this pins $h(6)=30$ exactly. See SAT/CP-SAT-based finite counterexample search and verification for the general "fix $n$, encode as CNF, UNSAT-with-certificate = finite proof" template, of which this is a headline instance. 3. Independent re-verification via formal proof. Because 17,300 CPU-hours of SAT search is not something a human can re-check by hand, Subercaseaux et al. (arXiv:2403.17370) rebuilt the *entire* SAT-encoding-to-geometry bridge inside the Lean theorem prover — not just checking the solver's DRAT/proof certificate, but formally re-deriving that the CNF encoding faithfully captures "order type has no empty hexagon," a strictly higher verification bar than typical computer-assisted-proof practice. This is itself a transferable template for any future Erdős–Szekeres-type SAT result: encode-and-solve, then *separately* formalize the encoding's correctness, so trust in the final numeral doesn't depend on trusting the solver or the encoding script by hand-inspection alone. 4. Why $k=6$ is the last case (portable boundary lesson). Horton's 1983 recursive construction shows the phenomenon is not "eventually true for all $k$" — it hard-stops at 6. Any future attempt to push empty-polygon-type Ramsey results to a new parameter regime should first check for a Horton-style recursive counterexample family before investing in an existence proof; this is the standard sanity check the field now runs first (per erdosproblems.com/216's remark structure and the survey literature on Erdős–Szekeres-type problems).

Related

- Erdős #107 — exact Erdős–Szekeres convex-polygon constant — the underlying (still-open) Erdős–Klein–Szekeres "happy ending" problem for ordinary (non-empty) convex polygons, $f(n)=2^{n-2}+1$; #216 is its "empty" variant and both proofs of #216's existence stage route through Erdős–Szekeres $\mathrm{ES}(n)$ as the covering black box. - SAT/CP-SAT-based finite counterexample search and verification — the general SAT-encode/UNSAT-certificate/formally-verify template; this wiki's existing concept page already documents the Heule–Scheucher and Subercaseaux et al. results in the same terms used here. - The alteration (deletion) method — probabilistic existence proofs that build an almost-good random structure, then delete its blemishes; canonical instance: Erdős's 1959 high-girth/high-chromatic-number graphs — contrast case: Horton's non-existence construction for $k\ge7$ is an explicit recursive/geometric construction rather than a probabilistic-deletion argument, useful as a "what technique family to try first" pointer for adjacent empty-polygon non-existence questions.