Erdős problem 487 · problems.science

Let $A\subseteq \mathbb{N}$ have positive density. Must there exist distinct $a,b,c\in A$ such that $[a,b]=c$ (where $[a,b]$ is the least common multiple of $a$ and $b$ )?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

487.lean

Retained formal statement1 of 1

Let $A\subseteq \mathbb{N}$ have positive density. Must there exist distinct $a,b,c\in A$ such that $[a,b]=c$ (where $[a,b]$ is the least common multiple of $a$ and $b$ )?

This is true, a consequence of the positive solution to [447] by Kleitman [Kl71].

Davenport and Erdős [DaEr36] showed that there must exist an infinite sequence $a_1<a_2\cdots$ in $A$ such that $a_i\mid a_j$ for all $i\leq j$ , under the assumption that the upper logarithmic density of $A$ is positive.

FormalConjectures/ErdosProblems/487.leanErdos487.erdos_4871 lineExact file

1True ↔ ∀ (A : Set ℕ), A.HasPosDensity → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, a ≠ b ∧ b ≠ c ∧ a ≠ c ∧ a.lcm b = c

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science