Erdős Problem #425

The question

erdos_425.parts.i. Let $F(n)$ be the maximum size of a subset of $\{1,\dots ,n\}$ with distinct pairwise products. Is there a constant $c>0$ such that $$F(n)=\pi (n)+(c+o(1))n^{3/4}(\log n{)}^{-3/2}?$$

erdos_425.parts.ii. If all products of $r$ distinct elements of $A\subseteq \{1,\dots ,n\}$ are distinct, must $$|A|\le \pi (n)+O\left(n^{(r+1)/(2r)}\right)?$$

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.ErdosProblems.«425» (2 statements).

theorem erdos_425.parts.i : ∃ c : ℝ, 0 < c ∧
    Tendsto
      (fun n : ℕ =>
        ((pairProductExtremal n : ℝ) - (Nat.primeCounting n : ℝ)) /
          ((n : ℝ) ^ ((3 : ℝ) / 4) * (Real.log n) ^ (-(3 : ℝ) / 2)))
      atTop (𝓝 c)

theorem erdos_425.parts.ii : ∀ r : ℕ, 1 ≤ r → ∃ C : ℝ, 0 < C ∧
    ∀ᶠ n in atTop, ∀ A : Finset ℕ, A ⊆ Finset.Icc 1 n → RProductsDistinct r A →
      (A.card : ℝ) ≤ (Nat.primeCounting n : ℝ) +
        C * (n : ℝ) ^ (((r : ℝ) + 1) / (2 * r))

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already — check erdosproblems.com/425. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

Erdős Problem 425

Source and licence

Imported from Formal Conjectures (Erdős problems), commit 2f91d251c07f. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.