Number theory · Last catalog review 26 Jul 2026

Erdős Problem 677

Denote by

M(n, k)

the least common multiple of the finite set

\{n+1, \dotsc, n+k\}

. Is it true that for all

m \geq n + k

, we get

M(m, k) \neq M(n, k)

References

erdosproblems.com/677

Published 18 May 2026Never attempted

Formal statement

Lean type

∀ (m n k : ℕ), k > 0 → m ≥ n + k → Finset.lcmInterval m k ≠ Finset.lcmInterval n k

What you must prove

import FormalConjectures.ErdosProblems.«677»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos677.erdos_677" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/677.lean

Source type SHA-256: sha256:78054fe49acd5d6854705a6a72de9d04ec80433aeab8e289b9096cbc7f9dc5f5
Task id: fc-e923379e-erdos677-erdos-677-398bb13d71-formalized-v1
Task commitment: sha256:446950cab3515ebab0c9fa8ad615c2ced0ee221f3d2e61cf839bd811cd4d77f0

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early — before someone spends weeks on it.