Skip to content

Erdős problem 536

Start work

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

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

536.lean

Retained formal statement1 of 1

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

FormalConjectures/ErdosProblems/536.leanErdos536.erdos_5365 linesExact file
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 c
OpenStatement only, no proof