ErdosProblems · research open · AMS 5 11

unsolvedsorry — nobody on it

Erdős Problem 535

Conjecture 535 · Erdős

Let r≥3r \geq 3, and let fr(N)f_r(N) denote the size of the largest subset of {1,…,N}\{1,\ldots,N\} such that no subset of size rr has the same pairwise greatest common divisor between all elements. Erdős [Er64] proved that f3(N)>Nc/log⁡log⁡Nf_3(N) > N^{c/\log\log N} for some constant c>0c > 0, and conjectured this should also be an upper bound; here we state the conjectural upper bound for all r≥3r \geq 3.

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
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗