Erdős problem 699

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)$ ?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

699.lean

Retained formal statement3 of 3

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

FormalConjectures/ErdosProblems/699.leanErdos699.sylvester_schur1 lineExact file

1∀ (n i : ℕ), 1 ≤ i → i ≤ n / 2 → ∃ p, Nat.Prime p ∧ i < p ∧ p ∣ n.choose i

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.