Conjectures.io

Number theory

Erdős 677

Denote by M(n,k)M(n, k) the least common multiple of the finite set {n+1,…,n+k}\{n+1, \dotsc, n+k\}. Is it true that for all m≥n+km \geq n + k, we get M(m,k)≠M(n,k)M(m, k) \neq M(n, k)?

References

No one has attempted this yet.

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-379fc029-erdos677-erdos-677-e0217e3866-formalized-v1
Task commitment
sha256:0f014b47e16a041989dc798e8c791d16b1c879e763bcaf01d911799cce8dccc9

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.