Erdős and Szekeres conjectured that, apart from a finite exceptional set of triples `(n, i, j)`,
one can always take `p > i` in the prime divisor statement.
Actions
Submit a Proof
Have a proof attempt? Submit it for zero-trust verification.
theorem erdos_szekeres_strengthening : answer(sorry) ↔
∃ E : Finset (ℕ × ℕ × ℕ), ∀ n i j : ℕ,
1 ≤ i →
i < j →
j ≤ n / 2 →
(n, i, j) ∉ E →
∃ p : ℕ, p.Prime ∧ i < p ∧ p ∣ Nat.gcd (Nat.choose n i) (Nat.choose n j)
