Skip to content

Erdős problem 678

Start work

Write M(n,k)M(n, k) be the least common multiple of {n+1,…,n+k}\{n+1, \dotsc, n+k\}. Let kk be sufficiently large. Are there infinitely many m,nm, n with m≥n+km \geq n + k such that M(n,k)>M(m,k+1) 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

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

678.lean

Retained formal statement2 of 7

The pairs (m,n)(m, n) with m≥n+km \geq n + k and M(n,k)>M(m,k+1)M(n, k) > M(m, k + 1) are infinite in number once kk is allowed to vary, which is the sense in which Cambie's result answers the question.

FormalConjectures/ErdosProblems/678.leanErdos678.erdos_678.variants.infinitely_many_triples1 lineExact file
{(k, m, n) | 3 ≤ k ∧ 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.