Erdős problem 535
Let , and let denote the size of the largest subset of such that no subset of size has the same pairwise greatest common divisor between all elements. Erdős [Er64] proved that for some constant , and conjectured this should also be an upper bound; here we state the conjectural upper bound for all .
Sources
FormalConjectures/ErdosProblems/
535.lean
Retained formal statement
Let , and let denote the size of the largest subset of such that no subset of size has the same pairwise greatest common divisor between all elements. Erdős [Er64] proved that for some constant , and conjectured this should also be an upper bound; here we state the conjectural upper bound for all .
See also [536].
∀ r ≥ 3, ∃ c > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos535.f r N) ≤ ↑N ^ (c / Real.log (Real.log ↑N))OpenStatement only, no proof