Erdős problem 443
Let . What is Is it for all sufficiently large ?
Sources
FormalConjectures/ErdosProblems/
443.lean
Retained formal statement
Let . What is Is it for all sufficiently large ?
This was solved independently by Hegyvári [He25] and Cambie (unpublished), who show that if then the set in question has size and that for any integer there exist infinitely many pairs such that the set in question has size .
True ↔ ∀ (ε : ℝ), 0 < ε → ∃ n₀, ∀ (m n : ℕ), n₀ < n → n < m → ↑(Erdos443.A n ∩ Erdos443.A m).card < (↑m * ↑n) ^ ε