Erdős problem 402 · problems.science

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

Sources

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

3 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

402.lean

Retained formal statement1 of 3

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

FormalConjectures/ErdosProblems/402.leanErdos402.erdos_4021 lineExact file

1∀ (A : Finset ℕ), 0 ∉ A → A.Nonempty → ∃ a ∈ A, ∃ b ∈ A, ↑(a.gcd b) ≤ ↑a / ↑A.card

SolvedStatement only, no proof