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

Worked, still open.

number theory · solved · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

formal

AMS 11 · solved (literature)

theorem erdos_402 (A : Finset ℕ) (h₁ : 0 ∉ A) (h₂ : A.Nonempty) : ∃ᵉ (a ∈ A) (b ∈ A),
    a.gcd b ≤ (a / A.card : ℚ)

solved