Erdős problem 536
Let and be sufficiently large. Is it true that if has size at least then there must be distinct such that where denotes the least common multiple?
Sources
FormalConjectures/ErdosProblems/
536.lean
Retained formal statement
Let and be sufficiently large. Is it true that if has size at least then there must be distinct such that where denotes the least common multiple?
True ↔ ∀ ε > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, ε * ↑N ≤ ↑A.card → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, {a, b, c}.card = 3 ∧ a.lcm b = b.lcm c ∧ b.lcm c = a.lcm cOpenStatement only, no proof