Erdős problem 678 · problems.science

Write $M(n, k)$ be the least common multiple of $\{n+1, \dotsc, n+k\}$ . Let $k$ be sufficiently large. Are there infinitely many $m, n$ with $m \geq n + k$ such that $M(n, k) > M(m, k + 1)$ ? The answer is yes, as proved in a strong form by Cambie [Ca24]. [Ca24] S. Cambie, Resolution of an Erdős' problem on least common multiples. arXiv:2410.09138 (2024).

Sources

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

7 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

678.lean

Retained formal statement3 of 7

For a fixed sufficiently large $k$ only finitely many pairs occur: $M(m, k + 1) \geq m + 1$ bounds $m$ by $M(n, k)$ , and for large $n$ the inequality reverses. So the question cannot be read as asking for infinitely many pairs at a single $k$ .

FormalConjectures/ErdosProblems/678.leanErdos678.erdos_678.variants.not_infinitely_many_pairs1 lineExact file

1¬∀ᶠ (k : ℕ) in Filter.atTop, {(m, n) | n + k ≤ m ∧ Finset.lcmInterval m (k + 1) < Finset.lcmInterval n k}.Infinite

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