Erdős problem 678
Write be the least common multiple of . Let be sufficiently large. Are there infinitely many with such that ? 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).
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/678.leanTrue ↔ ∀ᶠ (k : ℕ) in Filter.atTop, {(m, n) | n + k ≤ m ∧ Finset.lcmInterval m (k + 1) < Finset.lcmInterval n k}.NonemptyProof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:678 - PLBY Lean proofs
ErdosProblems.Erdos678
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine