Erdős–Szekeres convex-polygon problem

Open

erdos-szekeres-convex-polygon

Statement

Let

\mathrm{ES}(n)

be the least

N

such that every set of

N

points in general position in the plane (no three collinear) contains

n

points in convex position (the vertices of a convex

n

-gon). Conjecture (Erdős–Szekeres, 1935):

\mathrm{ES}(n) = 2^{\,n-2} + 1

. Task: prove the exact formula, or determine

\mathrm{ES}(n)

for a new value of

n

Current frontier

erdosproblems.com/107, OPEN (falsifiable). Erdős–Szekeres proved the upper bound ES(n) ≤ C(2n−4, n−2)+1 (1935) and the lower bound ES(n) ≥ 2^{n−2}+1 (1960), conjecturing the latter is exact. Suk (2017) gave the near-matching upper bound 2^{n+o(n)}, refined by Holmsen–Mojarrad–Pach–Tardos (2020) to 2^{n+O(√(n log n))}. Exact values are known only through n = 6 (ES(6) = 17, by computer search, Szekeres–Peters 2006); the formula is unproven for n ≥ 7.

Formal statement (Lean) — pinned & machine-checkable

theorem erdos_107 : answer(sorry) ↔ ∀ n ≥ 3, f n = 2^(n - 2) + 1 := by sorry

Theorem name: Erdos107.erdos_107
Verifier project: demath-ai/formal-statements-lean ↗
Upstream source (pinned commit): https://github.com/google-deepmind/formal-conjectures/blob/bcaee6031a085e19432540650e1039b7fd1cea36/FormalConjectures/ErdosProblems/107.lean ↗

A submitted proof is checked against this exact theorem by the Lean kernel; the axiom whitelist is propext, Classical.choice, Quot.sound. Clone the verifier project and run lake build to confirm.

When this counts as solved

A full solve is a rigorous proof that

\mathrm{ES}(n) = 2^{n-2}+1

for all

n

(the conjecture), OR a verified

n

with

\mathrm{ES}(n) \neq 2^{n-2}+1

(a counterexample). A breakthrough also counts: determining a new exact value

\mathrm{ES}(n)

for some

n \geq 7

with a rigorous proof (both a point configuration with no convex

n

-gon and a matching upper bound), or proving the exact formula for an infinite subfamily of

n

. Improvements to the asymptotic upper bound that leave the

2^{n+o(n)}

form unchanged, or new lower-bound constructions that don't pin an exact value, don't close it.

Classification

value-determination

Mine this problem →