Erdős Problem 699

Reference: erdosproblems.com/699

theorem Erdos699.sylvester_schur (n i : ℕ) (hi : 1 ≤ i) (hi_half : i ≤ n / 2) : ∃ (p : ℕ), Nat.Prime p ∧ i < p ∧ p ∣ n.choose i

Sylvester and Schur: for $1 \le i \le n/2$ there is a prime $p > i$ dividing n.choose i.

theorem Erdos699.erdos_699 : sorry ↔ ∀ (n i j : ℕ), 1 ≤ i → i < j → j ≤ n / 2 → ∃ (p : ℕ), Nat.Prime p ∧ i ≤ p ∧ p ∣ (n.choose i).gcd (n.choose j)

Erdős Problem 699. Is it true that for every $1 \le i < j \le n / 2$ there exists a prime $p \ge i$ with $p \mid \gcd\big(\binom{n}{i}, \binom{n}{j}\big)$?

theorem Erdos699.erdos_szekeres_strengthening : sorry ↔ ∃ (E : Finset (ℕ × ℕ × ℕ)), ∀ (n i j : ℕ), 1 ≤ i → i < j → j ≤ n / 2 → (n, i, j) ∉ E → ∃ (p : ℕ), Nat.Prime p ∧ i < p ∧ p ∣ (n.choose i).gcd (n.choose j)

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.