Erdős #107 — exact Erdős–Szekeres convex-polygon constant

Statement

Let $f(n)$ be minimal such that any $f(n)$ points in $\mathbb{R}^2$, no three on a line, contain $n$ points which form the vertices of a convex $n$-gon. Prove that $f(n) = 2^{n-2}+1$.

This is the Erdős–Klein–Szekeres "Happy Ending" problem (so named because Klein, who first observed $f(4)=5$ in 1931/33, later married Szekeres, one of the two mathematicians — with Erdős — who worked the problem out; the name is due to Erdős). Usually written $ES(n)$ in the literature.

Facts

- Prize \$500 for a proof; erdosproblems.com/107 (citing [Er97e]) notes Erdős only offered \$100 for a disproof. Ronald Graham additionally offered \$1000 for a proof [Gr04]. Status on the site: open, tagged FALSIFIABLE (a finite point set with $f(n)$ points but no convex $n$-gon, for some specific $n$, would falsify the conjectured exact value for that $n$). - Falsifiable: yes for any single $n$ (a finite counterexample set settles $f(n)=2^{n-2}+1$ false for that $n$), but a full proof is an infinite (for-all-$n$) statement. - Origin: Klein observed $f(4)=5$ (1931/33); Turán and Makai showed $f(5)=9$. Erdős and Szekeres proved $2^{n-2}+1 \leq f(n) \leq \binom{2n-4}{n-2}+1$ ([ErSz60] and [ErSz35] respectively) and conjectured the lower bound is tight. Restated across [Er61,p.245] [Er75f,p.106] [Er81] [Er82e] [Er83c] [Er95,p.184] [Er97c] [Er97e] [Va99,4.66]. - Lower bound (construction side, believed tight): $f(n) \geq 2^{n-2}+1$, via an explicit point-set construction due to Erdős–Szekeres [ErSz60]. Unimproved since 1960/61. - Upper bound chain (the side under active attack): - $f(n) \leq \binom{2n-4}{n-2}+1 = 4^{n-o(n)}$ — Erdős–Szekeres's original 1935 pigeonhole/Ramsey argument [ErSz35]. - Small constant-factor improvements over decades (surveyed in Suk's paper, arXiv:1604.08657, §1), all still of the form $4^{(1+o(1))n}$; best pre-2016 was $\limsup ES(n)/\binom{2n-4}{n-2} \leq 7/16$ (Norin–Yuditsky; Mojarrad–Vlachos). - Breakthrough: Andrew Suk, "On the Erdős-Szekeres convex polygon problem," J. Amer. Math. Soc. 30 (2017), 1047-1053, arXiv:1604.08657 — proves $f(n) \leq 2^{n+6n^{2/3}\log n}$, i.e. $f(n) = 2^{n+o(n)}$, matching the conjectured exponential base. Read in full: the proof combines the classical Erdős–Szekeres cup-cap theorem, the Pór–Valtr positive-fraction Erdős–Szekeres theorem (any point set of size $\geq 2^{32k}$ contains a $k$-cup/cap whose "support regions" each still hold a $1/2^{32k}$-fraction of the points), and Dilworth's theorem applied to a partial order induced on each support region, to push the base of the exponent from $4$ down to $2$. - Current best bound: Holmsen, Mojarrad, Pach, Tardos, "Two extensions of the Erdős-Szekeres problem," J. Eur. Math. Soc. 22 (2020), 3981-3995, arXiv:1710.11415 — $f(n) \leq 2^{n+O(\sqrt{n\log n})}$, sharpening Suk's error term and generalizing to convexity structures from pseudoline arrangements. - Small exact values: $f(3)=3$, $f(4)=5$, $f(5)=9$ (classical), $f(6)=17$ — established by an exhaustive computer search: L. Peters and G. Szekeres, "Computer solution to the 17-point Erdős-Szekeres problem," ANZIAM J. 48(2) (2006), 151-164 (cited in the SoCG 2025 reference list below). $f(7)$ is NOT known exactly — the conjecture predicts $f(7)=33$, and this is described as "the first open case of the planar Erdős–Szekeres problem" in Dumitru Bogdan, "Notes on the 33-point Erdős–Szekeres problem," arXiv:2512.24061 (Dec 2025) — a live, currently-unsolved SAT-search target. Martin Balko and Pavel Valtr, "A SAT attack on the Erdős–Szekeres conjecture," Eur. J. Combin. 66 (2017), 13-23 (SoCG 2017), used SAT solvers to disprove a stronger structural conjecture of Peters–Szekeres about 7-point configurations, but did not resolve $f(7)=33$ itself. - Formalized in Lean: yes, google-deepmind/formal-conjectures/FormalConjectures/ErdosProblems/107.lean — the exact conjecture erdos_107 is stated with proof sorry (fully open); the three known bound theorems (ersz_bounds, su_bound, hmpt_bound) are also stated but stubbed sorry (not yet formalized, despite being "research solved" in the literature) — a concrete, well-scoped formalization target. - Recent related work: Koki Furukawa, "Happy Ending or Many Concurrent Lines," arXiv:2409.03122 (2024) — line-arrangement analogue $ES_L(l,n)$ (concurrent lines vs. convex position for lines). Jineon Baek and Martin Balko, "The Erdős-Szekeres Conjecture Revisited," SoCG 2025 (DOI 10.4230/LIPIcs.SoCG.2025.13) — see Literature state below. - Related problems: Erdős #216 — the empty hexagon number g(6) (and non-existence for k≥7) Erdős #651 — higher-dimensional Erdős–Szekeres convex-position numbers are subexponential for d≥3 (disproved) Erdős #838 — f(n), the minimum number of distinct convex subsets of n points (open precise growth rate; two-sided quasi-polynomial bound SOLVED by Erdős 1978 via double counting against the Erdős–Szekeres theorem).

Literature state

Not resolved exactly, but very substantially resolved asymptotically. The precise formula $f(n)=2^{n-2}+1$ remains fully open (Lean proof is sorry); no source found claims a proof or disproof of the exact identity for general $n$. However: - Asymptotic near-resolution: Suk (2017, arXiv:1604.08657) proved $f(n)=2^{n+o(n)}$, matching the conjectured base $2$ exactly (the classical bound only gave base $4$). This is widely described (including by Suk himself, "we nearly settle the Erdős-Szekeres conjecture") as resolving the *order of growth* of the problem, leaving only the lower-order term and the exact additive constant open. Holmsen–Mojarrad–Pach–Tardos (2020, arXiv:1710.11415) sharpened the error term to $O(\sqrt{n\log n})$ and extended the method to pseudoline-arrangement convexity structures — the current state of the art on the upper bound. - Exact small cases: known up to $n=6$ ($f(6)=17$, Peters–Szekeres 2006 computer search). $n=7$ ($f(7)=33$ conjectured) is explicitly still open and under active SAT-solver attack as of December 2025 (Bogdan, arXiv:2512.24061) — this is the single most concrete, currently-live finite sub-target of the whole problem. - New structural progress (2025): Baek and Balko (SoCG 2025) prove the *exact* Erdős–Szekeres bound $2^{n-2}+1$ is tight for a relaxed notion they call a "split $k$-gon," prove the conjecture holds for a restricted class of "decomposable" point sets, and give new, more general constructions of $2^{k-2}$-point sets with no convex $k$-gon (generalizing all previously known extremal constructions) — explicitly enabling further computational attacks on the conjecture for larger $k$. They also show a natural hypergraph generalization of the conjecture is *false*, which is useful negative information about how far the proof technique can generalize. - No AI system (LLM, AlphaEvolve, Aristotle, DeepMind formal-conjectures) is credited with new mathematical progress on this problem; the formal-conjectures repo only records the statement, not a proof, of any of the four theorems (main conjecture + 3 known bound theorems). - The sister/"See also" problem Erdős #216 — the empty hexagon number g(6) (and non-existence for k≥7) (existence of an empty convex hexagon forced in every sufficiently large point set) is fully resolved: Gerken (Discrete Comput. Geom. 39 (2008), 239-272) and Nicolás (Discrete Comput. Geom. 38 (2007), 389-397) independently proved every point set of $\geq 30$ points contains an empty convex hexagon (i.e. $g(6)=30$, later confirmed exactly via computer/SAT and machine-checked: Marijn Heule, "Happy Ending: An Empty Hexagon in Every Set of 30 Points," arXiv:2403.00737 (2024), and "Formal Verification of the Empty Hexagon Number," arXiv:2403.17370), while Horton (1983) gave an explicit infinite construction with no empty convex heptagon, so $g(k)$ is infinite for all $k\geq 7$. This shows the exact sibling question (small-hole existence) was fully cracked by exactly the SAT-search + formal-verification pipeline that Balko–Valtr and Bogdan are now applying to $f(7)$ — the clearest evidence for where the tractable win on #107 currently sits.

Attack surface

- Mode: finite-search (for the concrete $f(7)=33$ sub-case) + literature-resolution/derivation (for tracking/extending the asymptotic bound and formalizing known results). - Concrete first experiment: replicate/extend the Balko–Valtr / Bogdan SAT encoding for $ES(7)$ — encode a 33-or-34-point configuration via triple-orientation (order-type) Boolean variables, add the 4-set convexity criterion to forbid any 7 points in convex position, add convex-layer/anchoring symmetry-breaking constraints (as in arXiv:2512.24061), and run a modern CDCL/cube-and-conquer SAT solver (the same class of tooling — Heule et al.'s march_cu / cube-and-conquer — that resolved the sister empty-hexagon problem, arXiv:2403.00737) to try to either (a) find a 34-point counterexample set with no convex 7-gon (disproof, \$100, and would falsify the whole conjecture), or (b) push the UNSAT certificate to fully cover all anchored subfamilies and thereby nail down $f(7)=33$ (a genuine, citable, currently-open partial result — Bogdan's Dec-2025 paper reports this is *not yet complete*, blocked on heavy-tailed runtime variance). - Oracle: fully mechanical — an order-type/SAT model directly encodes point-set combinatorics (realizability via an order-type database, e.g. Aichholzer et al.'s order-type data, or direct SAT satisfiability of orientation-consistency + convexity constraints); UNSAT with a proof certificate (DRAT) is machine-checkable, and any candidate SAT witness (point coordinates) can be numerically verified for convex-position-freeness in polynomial time. - Feasibility: honest read — the exact conjecture for general $n$ is famous and hard (open since 1935/1960, resisted Erdős, Suk, HMPT, Baek–Balko), but the $f(7)=33$ sub-case is a live, well-scoped, currently-open computational target actively being attacked with SAT solvers right now (Dec 2025 paper, unresolved) — this is squarely in reach for a serious SAT/order-type engineering effort, directly analogous to how Heule et al. closed the $g(6)=30$ empty-hexagon case in 2024. A win here would not collect the \$500 (that requires the general-$n$ proof) but would be a genuine, citable, formalizable result and the most concrete lever on this problem.

Related

- Erdős #216 — the empty hexagon number g(6) (and non-existence for k≥7) — sister "Happy Ending" problem (empty convex $k$-gons instead of $k$-gons in convex position); fully resolved ($g(6)=30$ Gerken/Nicolás/Heule, $g(k)=\infty$ for $k\geq7$ Horton) via the exact SAT-search + order-type pipeline that is the recommended attack route for #107's $f(7)$ sub-case. - Erdős #651 — higher-dimensional Erdős–Szekeres convex-position numbers are subexponential for d≥3 (disproved) — higher-dimensional analogue: $f_k(n)$, minimal points in $\mathbb{R}^k$ in general position forcing $n$ in convex position; asks for exponential lower bound $f_k(n) > (1+c_k)^n$. - Erdős #838 — f(n), the minimum number of distinct convex subsets of n points (open precise growth rate; two-sided quasi-polynomial bound SOLVED by Erdős 1978 via double counting against the Erdős–Szekeres theorem) — related extremal question: minimum number of *distinct* convex subsets determined by $n$ points in the plane. - Erdős–Szekeres cup-cap (cap-cup) theorem: exact Ramsey number for convex chains — Erdős–Szekeres's original 1935 combinatorial lemma ($f(k,\ell)=\binom{k+\ell-4}{k-2}+1$ for forcing a $k$-cup or $\ell$-cap), the base tool for every upper bound in this family, including Suk's. - Pór–Valtr positive-fraction Erdős–Szekeres theorem: dense clusters, not just points, in convex position — Pór–Valtr's theorem (any large point set contains a $k$-cup/cap whose support regions each retain a positive fraction of the points); the key new ingredient Suk used to reach base-$2$. - Dilworth's theorem (chain/antichain decomposition of a poset) and its dual, Mirsky's theorem — chain/antichain decomposition applied to the partial order induced on each support region in Suk's proof. - Order type / orientation encoding of planar point sets (CC-systems, chirotopes, and the Aichholzer–Aurenhammer–Krasser database) / SAT/CP-SAT-based finite counterexample search and verification — order-type/orientation SAT encodings used by Balko–Valtr (2017) and Bogdan (2025) to attack $f(7)$, and by Heule et al. (2024) to fully resolve the sister empty-hexagon number $g(6)=30$. - Baek–Balko split k-gon relaxation: an exactly-tight 2^{k-2}+1 threshold for a weakening of convex position — Baek–Balko's (SoCG 2025) relaxed convexity notion for which the exact $2^{k-2}+1$ threshold is proven tight, plus their new generalized extremal constructions enabling further computation. - Lean 4 formalization of constructions and conditional reductions (Erdős-problem context) — google-deepmind/formal-conjectures project; conjecture and all three known bound theorems stated but sorryd, a concrete formalization target.