Documentation

FormalConjectures.ErdosProblems.«536»

Erdős Problem 536 #

Reference: erdosproblems.com/536

theorem Erdos536.erdos_536 :
(∀ ε > 0, ∀ᶠ (N : ) in Filter.atTop, AFinset.Icc 1 N, ε * N A.cardaA, bA, cA, {a, b, c}.card = 3 a.lcm b = b.lcm c b.lcm c = a.lcm c) sorry

Let $\epsilon>0$ and $N$ be sufficiently large. Is it true that if $A\subseteq \{1,\ldots,N\}$ has size at least $\epsilon N$ then there must be distinct $a,b,c\in A$ such that $$[a, b]=[b, c]=[a, c],$$ where $[\cdot, \cdot]$ denotes the least common multiple?