Distinct multiples in an interval

DefinitionDistinct multiples of \(1, \dots, n\) in an interval#✓fully proved

For natural numbers \(n\), \(m\) and \(L\), the interval \((m, m + L]\) contains distinct multiples of \(1, \dots, n\) when there are pairwise distinct natural numbers \(a_1, \dots, a_n\) with \(m < a_i \le m + L\) and \(i \mid a_i\) for every \(1 \le i \le n\).

def HasDistinctMultiplesInInterval (n m L : ℕ) : Prop :=
  ∃ a : Fin n → ℕ, Function.Injective a ∧
    ∀ i : Fin n, m < a i ∧ a i ≤ m + L ∧ (i.val + 1) ∣ a i

Sources

Wouter van Doorn, On the Length of an Interval That Contains Distinct Multiples of the First n Positive Integers, INTEGERS 26 (2026), Article A7, Section 1 (definition of f(n, m), after Erdős and Pomerance).

Used by 6

Used byLeast interval length containing distinct multiples · Characterization of the least interval length · The least interval length for \(n = 1\) · Some interval contains distinct multiples · The least interval length is admissible · Lengthening the interval preserves distinct multiples

DefinitionLeast interval length containing distinct multiples#✓fully proved

For natural numbers \(n\) and \(m\), \(f(n, m)\) is the least natural number \(L\) such that the interval \((m, m + L]\) contains distinct multiples of \(1, \dots, n\).

Such an \(L\) always exists, so the least one is well defined.

noncomputable def distinctMultiplesIntervalLength (n m : ℕ) : ℕ :=
  sInf {L | HasDistinctMultiplesInInterval n m L}

def HasDistinctMultiplesInInterval (n m L : ℕ) : Prop :=
  ∃ a : Fin n → ℕ, Function.Injective a ∧
    ∀ i : Fin n, m < a i ∧ a i ≤ m + L ∧ (i.val + 1) ∣ a i

MathlibExt/NumberTheory/DistinctMultiplesInterval.lean:36

Sources

Wouter van Doorn, On the Length of an Interval That Contains Distinct Multiples of the First n Positive Integers, INTEGERS 26 (2026), Article A7, Section 1 (definition of f(n, m), after Erdős and Pomerance).

Uses 1 · Used by 6

Statement usesDistinct multiples of \(1, \dots, n\) in an interval

Used byErdős–Pomerance bounds for the diagonal interval length · Characterization of the least interval length · An inequality between diagonal and shifted interval lengths · The least interval length for \(n = 1\) · Shifting the interval can greatly increase the least length · The least interval length is admissible

TheoremLengthening the interval preserves distinct multiples#✓fully proved

For natural numbers \(n\), \(m\), \(L\) and \(L'\) with \(L \le L'\), if the interval \((m, m + L]\) contains distinct multiples of \(1, \dots, n\), then so does the interval \((m, m + L']\).

theorem HasDistinctMultiplesInInterval.mono {n m L L' : ℕ} (hLL' : L ≤ L')
    (h : HasDistinctMultiplesInInterval n m L) : HasDistinctMultiplesInInterval n m L'

def HasDistinctMultiplesInInterval (n m L : ℕ) : Prop :=
  ∃ a : Fin n → ℕ, Function.Injective a ∧
    ∀ i : Fin n, m < a i ∧ a i ≤ m + L ∧ (i.val + 1) ∣ a i

MathlibExt/NumberTheory/DistinctMultiplesInterval.lean:36

Sources

Wouter van Doorn, On the Length of an Interval That Contains Distinct Multiples of the First n Positive Integers, INTEGERS 26 (2026), Article A7, Section 1 (definition of f(n, m)).

Uses 1 · Used by 1

Statement usesDistinct multiples of \(1, \dots, n\) in an interval

Used byCharacterization of the least interval length

TheoremSome interval contains distinct multiples#✓fully proved

For all natural numbers \(n\) and \(m\) there is a natural number \(L\) such that the interval \((m, m + L]\) contains distinct multiples of \(1, \dots, n\).

For example, \(L = n(m + 1)\) works, with \(a_i = i(m + 1)\) for \(1 \le i \le n\).

theorem exists_hasDistinctMultiplesInInterval (n m : ℕ) :
    ∃ L, HasDistinctMultiplesInInterval n m L

def HasDistinctMultiplesInInterval (n m L : ℕ) : Prop :=
  ∃ a : Fin n → ℕ, Function.Injective a ∧
    ∀ i : Fin n, m < a i ∧ a i ≤ m + L ∧ (i.val + 1) ∣ a i

MathlibExt/NumberTheory/DistinctMultiplesInterval.lean:36

Sources

Wouter van Doorn, On the Length of an Interval That Contains Distinct Multiples of the First n Positive Integers, INTEGERS 26 (2026), Article A7, Section 1 (definition of f(n, m)).

Uses 1 · Used by 1

Statement usesDistinct multiples of \(1, \dots, n\) in an interval

Used byThe least interval length is admissible

TheoremThe least interval length is admissible#✓fully proved

For natural numbers \(n\) and \(m\), let \(f(n, m)\) be the least natural number \(L\) such that the interval \((m, m + L]\) contains distinct multiples of \(1, \dots, n\). Then the interval \((m, m + f(n, m)]\) contains distinct multiples of \(1, \dots, n\).

theorem hasDistinctMultiplesInInterval_distinctMultiplesIntervalLength (n m : ℕ) :
    HasDistinctMultiplesInInterval n m (distinctMultiplesIntervalLength n m)

def HasDistinctMultiplesInInterval (n m L : ℕ) : Prop :=
  ∃ a : Fin n → ℕ, Function.Injective a ∧
    ∀ i : Fin n, m < a i ∧ a i ≤ m + L ∧ (i.val + 1) ∣ a i

MathlibExt/NumberTheory/DistinctMultiplesInterval.lean:36

noncomputable def distinctMultiplesIntervalLength (n m : ℕ) : ℕ :=
  sInf {L | HasDistinctMultiplesInInterval n m L}

MathlibExt/NumberTheory/DistinctMultiplesInterval.lean:46

Sources

Wouter van Doorn, On the Length of an Interval That Contains Distinct Multiples of the First n Positive Integers, INTEGERS 26 (2026), Article A7, Section 1 (definition of f(n, m)).

Uses 3 · Used by 1

Statement usesDistinct multiples of \(1, \dots, n\) in an interval · Least interval length containing distinct multiples

Proof usesSome interval contains distinct multiples

Used byCharacterization of the least interval length

TheoremCharacterization of the least interval length#✓fully proved

For natural numbers \(n\) and \(m\), let \(f(n, m)\) be the least natural number \(K\) such that the interval \((m, m + K]\) contains distinct multiples of \(1, \dots, n\). Then for every natural number \(L\), \(f(n, m) \le L\) if and only if the interval \((m, m + L]\) contains distinct multiples of \(1, \dots, n\).

theorem distinctMultiplesIntervalLength_le_iff {n m L : ℕ} :
    distinctMultiplesIntervalLength n m ≤ L ↔ HasDistinctMultiplesInInterval n m L

noncomputable def distinctMultiplesIntervalLength (n m : ℕ) : ℕ :=
  sInf {L | HasDistinctMultiplesInInterval n m L}

MathlibExt/NumberTheory/DistinctMultiplesInterval.lean:46

def HasDistinctMultiplesInInterval (n m L : ℕ) : Prop :=
  ∃ a : Fin n → ℕ, Function.Injective a ∧
    ∀ i : Fin n, m < a i ∧ a i ≤ m + L ∧ (i.val + 1) ∣ a i

MathlibExt/NumberTheory/DistinctMultiplesInterval.lean:36

Sources

Wouter van Doorn, On the Length of an Interval That Contains Distinct Multiples of the First n Positive Integers, INTEGERS 26 (2026), Article A7, Section 1 (definition of f(n, m)).

Uses 4

Statement usesDistinct multiples of \(1, \dots, n\) in an interval · Least interval length containing distinct multiples

Proof usesLengthening the interval preserves distinct multiples · The least interval length is admissible

TheoremThe least interval length for \(n = 1\)#✓fully proved

For natural numbers \(n\) and \(m\), let \(f(n, m)\) be the least natural number \(L\) such that the interval \((m, m + L]\) contains distinct multiples of \(1, \dots, n\). Then \(f(1, m) = 1\) for every natural number \(m\): the interval \((m, m + 1]\) contains the multiple \(m + 1\) of \(1\), and the empty interval \((m, m]\) contains nothing.

theorem distinctMultiplesIntervalLength_one (m : ℕ) :
    distinctMultiplesIntervalLength 1 m = 1

Sources

Wouter van Doorn, On the Length of an Interval That Contains Distinct Multiples of the First n Positive Integers, INTEGERS 26 (2026), Article A7, Section 1 (definition of f(n, m)).

Uses 2

Statement usesLeast interval length containing distinct multiples

Proof usesDistinct multiples of \(1, \dots, n\) in an interval

TheoremAn inequality between diagonal and shifted interval lengths#●ready to prove

For natural numbers \(n\) and \(m\), let \(f(n, m)\) be the least natural number \(L\) such that the interval \((m, m + L]\) contains distinct multiples of \(1, \dots, n\). Then for all positive integers \(k\) and \(n\), \(kn + f(kn, kn) \le k^2 n + f(n, k^2 n)\).

public theorem_wanted distinctMultiplesIntervalLength_mul_le {k n : ℕ} (hk : 0 < k)
    (hn : 0 < n) :
    k * n + distinctMultiplesIntervalLength (k * n) (k * n) ≤
      k ^ 2 * n + distinctMultiplesIntervalLength n (k ^ 2 * n)

Sources

Wouter van Doorn, On the Length of an Interval That Contains Distinct Multiples of the First n Positive Integers, INTEGERS 26 (2026), Article A7, Lemma 2.

Uses 1

Statement usesLeast interval length containing distinct multiples

TheoremErdős–Pomerance bounds for the diagonal interval length#●ready to prove

For natural numbers \(n\) and \(m\), let \(f(n, m)\) be the least natural number \(L\) such that the interval \((m, m + L]\) contains distinct multiples of \(1, \dots, n\). For every real \(\varepsilon > 0\) and all sufficiently large natural numbers \(n\),

\[ \left(\frac{2}{\sqrt{e}} - \varepsilon\right) n \sqrt{\frac{\log n}{\log \log n}} < f(n, n) < (2 + \varepsilon)\, n \sqrt{\log n}. \]

public theorem_wanted distinctMultiplesIntervalLength_diag_bounds (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ n : ℕ in Filter.atTop,
      (2 / Real.sqrt (Real.exp 1) - ε) * n * Real.sqrt (Real.log n / Real.log (Real.log n)) <
          distinctMultiplesIntervalLength n n ∧
        (distinctMultiplesIntervalLength n n : ℝ) < (2 + ε) * n * Real.sqrt (Real.log n)

Sources

the constants are read from the paper text (arXiv:2601.16972, same paper, Lemma 3), since the record's are garbled; they agree with the record's √2e > 1.21 remark (2/√e ≈ 1.213).
Wouter van Doorn, On the Length of an Interval That Contains Distinct Multiples of the First n Positive Integers, INTEGERS 26 (2026), Article A7, Lemma 3, quoting Erdős and Pomerance.

Uses 1

Statement usesLeast interval length containing distinct multiples

TheoremShifting the interval can greatly increase the least length#●ready to prove

For natural numbers \(n\) and \(m\), let \(f(n, m)\) be the least natural number \(L\) such that the interval \((m, m + L]\) contains distinct multiples of \(1, \dots, n\). For all sufficiently large natural numbers \(n\) there is a positive integer \(m\) with

\[ f(n, m) - f(n, n) > \frac{0.36\, n \log n}{\log \log n}. \]

Since \(f(n, m)\) is periodic in \(m\) with period \(\operatorname{lcm}(1, \dots, n)\), this says that \(\max_{m \ge 1} f(n, m) - f(n, n) > 0.36\, n \log n / \log \log n\) for all large \(n\), the form stated in the source.

public theorem_wanted exists_distinctMultiplesIntervalLength_sub_gt :
    ∀ᶠ n : ℕ in Filter.atTop, ∃ m : ℕ, 0 < m ∧
      0.36 * (n : ℝ) * Real.log n / Real.log (Real.log n) <
        (distinctMultiplesIntervalLength n m : ℝ) - distinctMultiplesIntervalLength n n

Sources

Wouter van Doorn, On the Length of an Interval That Contains Distinct Multiples of the First n Positive Integers, INTEGERS 26 (2026), Article A7, Theorem 1.

Uses 1

Statement usesLeast interval length containing distinct multiples

DefinitionErdős's matching function for multiples in intervals#✓fully proved

For a natural number \(m\), \(f(m)\) is the largest natural number \(r\) such that for every natural number \(N\), every set \(A \subseteq \{1, \dots, N\}\) with exactly \(m\) elements and every real \(x \ge 1\), there are distinct \(a_1, \dots, a_r \in A\) and distinct natural numbers \(b_1, \dots, b_r\) in the open interval \((x, x + 2N)\) with \(a_i \mid b_i\) for every \(i\).

noncomputable def f (m : ℕ) : ℕ :=
  sSup {r : ℕ | ∀ N : ℕ, ∀ A ⊆ Finset.Icc 1 N, A.card = m → ∀ x : ℝ, 1 ≤ x →
    ∃ a b : Fin r → ℕ, Function.Injective a ∧ Function.Injective b ∧
      (∀ i, a i ∈ A) ∧ (∀ i, (b i : ℝ) ∈ Set.Ioo x (x + 2 * (N : ℝ))) ∧
      (∀ i, a i ∣ b i)}

Used by 1

Used byStatement of Erdős Problem 650

DefinitionStatement of Erdős Problem 650#✓fully proved

Let \(f\) be Erdős's matching function for multiples in intervals. The statement is the conjunction of four claims: for every natural number \(m\), \(f(m) = \min(m, \lceil 2\sqrt{m}\,\rceil)\); it is not the case that \(f(m) \le \sqrt{m}\) for every natural number \(m\); \(\sqrt{m} \le f(m)\) for every natural number \(m\); and \(f(m^2) \le 2m\) for every natural number \(m\).

def conjecture : Prop :=
  (∀ m : ℕ, f m = min m ⌈2 * Real.sqrt m⌉₊) ∧
  (¬ ∀ m : ℕ, (f m : ℝ) ≤ Real.sqrt m) ∧
  (∀ m : ℕ, Real.sqrt m ≤ (f m : ℝ)) ∧
  (∀ m : ℕ, f (m ^ 2) ≤ 2 * m)

noncomputable def f (m : ℕ) : ℕ :=
  sSup {r : ℕ | ∀ N : ℕ, ∀ A ⊆ Finset.Icc 1 N, A.card = m → ∀ x : ℝ, 1 ≤ x →
    ∃ a b : Fin r → ℕ, Function.Injective a ∧ Function.Injective b ∧
      (∀ i, a i ∈ A) ∧ (∀ i, (b i : ℝ) ∈ Set.Ioo x (x + 2 * (N : ℝ))) ∧
      (∀ i, a i ∣ b i)}

WantedExt/NumberTheory/ErdosProblem650Wanted.lean:35

Uses 1 · Used by 1

Statement usesErdős's matching function for multiples in intervals

Used byErdős Problem 650: matching integers to distinct multiples

TheoremErdős Problem 650: matching integers to distinct multiples#●ready to prove

For a natural number \(m\), let \(f(m)\) be the largest natural number \(r\) such that for every natural number \(N\), every set \(A \subseteq \{1, \dots, N\}\) with exactly \(m\) elements and every real \(x \ge 1\), there are distinct \(a_1, \dots, a_r \in A\) and distinct natural numbers \(b_1, \dots, b_r\) in the open interval \((x, x + 2N)\) with \(a_i \mid b_i\) for every \(i\). Then \(f(m) = \min(m, \lceil 2\sqrt{m}\,\rceil)\) for every natural number \(m\); it is not the case that \(f(m) \le \sqrt{m}\) for every natural number \(m\); \(\sqrt{m} \le f(m)\) for every natural number \(m\); and \(f(m^2) \le 2m\) for every natural number \(m\).

Solved by Erdős–Surányi [ErSu59], Erdős–Selfridge [Er78], [Er86c] and van Doorn–Li–Tang [VLT26].

public theorem_wanted conjecture_holds : conjecture

def conjecture : Prop :=
  (∀ m : ℕ, f m = min m ⌈2 * Real.sqrt m⌉₊) ∧
  (¬ ∀ m : ℕ, (f m : ℝ) ≤ Real.sqrt m) ∧
  (∀ m : ℕ, Real.sqrt m ≤ (f m : ℝ)) ∧
  (∀ m : ℕ, f (m ^ 2) ≤ 2 * m)

WantedExt/NumberTheory/ErdosProblem650Wanted.lean:42

Sources

[VLT26] W. van Doorn, Y. Li and Q. Tang, Optimal bounds for an Erdős problem on matching integers to distinct multiples, arXiv:2603.28636 (2026), https://arxiv.org/abs/2603.28636; W. van Doorn, Lean formalization of Erdős Problem 650 (Aristotle-assisted), https://github.com/Woett/Lean-files/blob/c100ed4a4429e987a9555ee428a1aa524a46e16d/ErdosProblem650.lean.

Uses 1

Statement usesStatement of Erdős Problem 650

9 fully proved4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.