erdos_szekeres_conjecture
Disprovedcombinatoricsgeometry
The Erdős–Szekeres conjecture (1935): ES(k) = 2^{k−2} + 1, i.e., any set of 2^{k-2}+1 points in general position in ℝ² contains k points in convex position, and this is tight. Proved for k ≤ 6 (the k=4 case is the 'happy ending'); the exact value 2^{k-2}+1 for k ≥ 7 is open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem erdos_szekeres_conjecture (k : ℕ) (hk : 3 ≤ k) :
∃ (N : ℕ) (_ : N = 2 ^ (k - 2) + 1),
∀ (pts : Fin N → ℝ × ℝ),
Function.Injective pts →
(∀ i j m : Fin N, i ≠ j → j ≠ m → i ≠ m →
¬ ∃ t : ℝ, 0 < t ∧ t < 1 ∧
pts m = ((pts i).1 + t * ((pts j).1 - (pts i).1),
(pts i).2 + t * ((pts j).2 - (pts i).2))) →
∃ (S : Finset (Fin N)) (_ : S.card = k),
∀ i ∈ S, ∀ j ∈ S, ∀ m ∈ S,
i ≠ j → j ≠ m → i ≠ m →
¬ ∃ t : ℝ, 0 < t ∧ t < 1 ∧
pts m = ((pts i).1 + t * ((pts j).1 - (pts i).1),
(pts i).2 + t * ((pts j).2 - (pts i).2)) → False := by
sorrySource