Erdős problem 699
Erdős Problem 699. Is it true that for every there exists a prime with ?
Sources
FormalConjectures/ErdosProblems/
699.lean
Retained formal statement
Erdős Problem 699. Is it true that for every there exists a prime with ?
True ↔ ∀ (n i j : ℕ), 1 ≤ i → i < j → j ≤ n / 2 → ∃ p, Nat.Prime p ∧ i ≤ p ∧ p ∣ (n.choose i).gcd (n.choose j)OpenStatement only, no proof