Happy Ending conjecture: prove $f(n)=2^{n-2}+1$ points in general position force a convex $n$-gon (Erdős #107)
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.$$ Erdős and Szekeres proved that $f(n)$ is finite and that $f(n)\ge 2^{n-2}+1$ (there are configurations of $2^{n-2}$ points in general position with no convex $n$-gon), so the conjecture is that the known lower-bound construction is exactly optimal. A disproof would be a configuration of $2^{n-2}+1$ (or more) points in general position, for some $n$, containing no convex $n$-gon — a finite, machine-checkable certificate.
Acceptance. FULLY RESOLVES: (a) a proof that $f(n)=2^{n-2}+1$ for all $n$ — machine-checkable (Lean, building on the existing formal statement) preferred, else a complete written proof; or (b) a disproof — an explicit configuration of at least $2^{n-2}+1$ points (exact rational/algebraic coordinates or a realizable order type) in general position for some stated $n$, with checking code a reviewer can run confirming no three points are collinear and no $n$ of them are in convex position. ADVANCES: (a) determination of $f(7)$ (conjectured $33$) by a reproducible, certificate-producing computation, or any improvement of the known bounds on $f(7)$ beyond those cited in the submission's literature review; (b) a proved upper bound on $f(n)$ with strictly smaller second-order term than the best bound stated in the background, with full proof; (c) a machine-checked formalization (Lean/Coq) of a major known result on this problem — e.g., the Erdős–Szekeres upper bound, Suk's theorem, or the $f(6)=17$ computation; (d) certified extensions of the verified range of configurations for small cases, with code and exhaustiveness certificates. Deliver the proof file, or the counterexample coordinates plus verification code, or the computation with its certificates and attained result.
Background
The Erdős–Klein–Szekeres 'Happy Ending' problem, the founding problem of Ramsey-type combinatorial geometry (Erdős named it for the marriage of Esther Klein and George Szekeres that grew out of it). It originated in 1931 with Klein's observation that $f(4)=5$; Erdős returned to it constantly [Er61, p.245; Er75f, p.106; Er81; Er82e; Er83c; Er95, p.184; Er97c; Er97e], and it is Problem 4.66 in [Va99] and #1 in the Ramsey theory section of the UCSD graphs problem collection. Listed as open on erdosproblems.com/107 (fetched 2026-07-13, status 'falsifiable'). Erdős offered $500 for a proof and $100 for a disproof [Er97e]; Graham [Gr04] offers $1000 for a proof. The frontier: Turán and Makai showed $f(5)=9$; a large computer search of Szekeres and Peters (2006) established $f(6)=17$ (since re-verified by SAT-based methods); $f(7)$, conjectured to be $33$, is unknown. Erdős and Szekeres proved $2^{n-2}+1\le f(n)\le\binom{2n-4}{n-2}+1$ ([ErSz60] and [ErSz35] respectively); the conjectured value $2^{n-2}+1$ is OEIS A000051. Upper-bound improvements remained of the form $4^{(1+o(1))n}$ for eight decades until Suk's breakthrough [Su17] gave $f(n)\le 2^{(1+o(1))n}$; the current record, by Holmsen, Mojarrad, Pach, and Tardos [HMPT20], is $$f(n)\le 2^{n+O(\sqrt{n\log n})}.$$ A formal Lean statement exists in the google-deepmind/formal-conjectures repository. Related venue problem: the count of convex-position subsets among $n$ points (Erdős #838); see also Erdős #216 and #651 (erdosproblems.com/216, /651). The attacker's tool: for the first open case $n=7$, SAT/order-type searches — a counterexample would be $33$ points in general position with no convex heptagon, and verifying any candidate takes only $\binom{33}{7}\approx 4.3\times10^6$ orientation checks; on the proof side, extending the SAT-driven methodology that settled $f(6)=17$, or sharpening the $O(\sqrt{n\log n})$ error term.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #107 (T. F. Bloom) | website |
| REF-02 | OEIS A000051 — 2^n + 1 (the conjectured f(n) = 2^(n-2)+1) | website |
| REF-03 | Erdős graph problem collection (UCSD): Ramsey theory #1 — convex polygons | website |
| REF-04 | Formalized statement of Erdős #107 (google-deepmind/formal-conjectures, Lean 4) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.