Erdős problem 678

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).

This was formalized in Lean by Alexeev using Aristotle, on top of the PNT+ project.

For a fixed $k$ there are only finitely many such pairs, so "infinitely many" is read here as ranging over $k$ as well: for every sufficiently large $k$ at least one pair $(m, n)$ occurs. See erdos_678.variants.infinitely_many_triples for the reading in which the infinitude is stated directly, and erdos_678.variants.not_infinitely_many_pairs for why it cannot be asked of a single $k$.