ErdosProblems · research open · AMS 5 11
unsolvedsorry — nobody on it
Erdős Problem 535
Conjecture 535 · Erdős
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].
Formal statement · Lean 4.lean
theorem erdos_535 : ∀ r ≥ 3, ∃ c > (0 : ℝ),
∀ᶠ (N : ℕ) in atTop,
(f r N : ℝ) ≤ (N : ℝ) ^ (c / log (log (N : ℝ))) := by
sorryProof. sorry
Nobody has tried yet.