Skip to content

Erdős problem 402

Prove that, for any finite set ANA\subset\mathbb{N}, there exist a,bAa, b\in A such that gcd(a,b)a/A. \gcd(a, b)\leq a/|A|.

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

402.lean

Retained formal statement3 of 3

Proved for all sufficiently large sets (including the sharper version which characterises the case of equality) independently by Szegedy [Sz86] and Zaharescu [Za87]. The following is taken from [Sz86].

There exists an effectively computable n0n_0 with the following properties: (i) if nn0n \ge n_0 and a1,a2,,ana_1, a_2, \dots, a_n are distinct natural numbers then maxi,jai(ai,aj)n\max_{i, j} \frac{a_i}{(a_i, a_j)} \ge n. (ii) If equality holds then the system {a1,a2,,an}\{a_1, a_2, \dots, a_n\} is either of the type {k,2k,,nk}\{k, 2k, \dots, nk\} or of the type {k1,k2,,kn}\left\{\frac{k}{1}, \frac{k}{2}, \dots, \frac{k}{n}\right\}.

FormalConjectures/ErdosProblems/402.leanErdos402.erdos_402.variants.szegedy_zaharescu_weak9 linesExact file
∀ᶠ (n : ℕ) in Filter.atTop,  ∀ (A : Finset ℕ),    A.card = n      0 ∉ A        (n ≤ (A ×ˢ A).sup fun x => x.1 / x.1.gcd x.2) ∧          ((n = (A ×ˢ A).sup fun x => x.1 / x.1.gcd x.2) ↔k > 0,              A = Finset.image (fun x => k * x) (Finset.Icc 1 n) ∨                A = Finset.image (fun x => k * (Finset.Icc 1 n).lcm id / x) (Finset.Icc 1 n))
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page