FormalConjectures.ErdosProblems.«375»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil
import FormalConjectures.Wikipedia.LegendreConjecture

Erdős Problem 375

References:

erdosproblems.com/375

[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

[RST75] Ramachandra, K. and Shorey, T. N. and Tijdeman, R., On Grimm's problem relating to factorisation of a block of consecutive integers. J. Reine Angew. Math. (1975), 109-124.


open Set Filter Topology Asymptotics


namespace Erdos375

This is a proposition saying that for any n ≥ 1 and any k, if n + 1, ..., n + k are all composite, then there are distinct primes p₁, ... pₖ such that pᵢ ∣ n + i for all 1 ≤ i ≤ k.

def Erdos375Prop : Prop := ∀ n ≥ 1, ∀ k, (∀ i < k, ¬ (n + i + 1).Prime) →
    ∃ p : Fin k → ℕ, p.Injective ∧ ∀ i, (p i).Prime ∧ p i ∣ n + i + 1

Is Erdos375Prop true?

@[category research open, AMS 11]
theorem declaration uses 'sorry'erdos_375 : answer(sorry) ↔ Erdos375Prop := by⊢ True ↔ Erdos375Prop
  sorryAll goals completed! 🐙

If Erdos375Prop is true, then (n + 1).nth Prime - n.nth Prime < (n.nth Prime) ^ (1 / 2 - c) for some c > 0.

@[category research solved, AMS 11]
theorem declaration uses 'sorry'erdos_375.variants.bounded_gap : Erdos375Prop →
    ∃ c > 0, ∀ᶠ n in atTop, (n + 1).nth Nat.Prime - n.nth Nat.Prime
    < (n.nth Nat.Prime : ℝ) ^ (1 / (2 : ℝ) - c) := by⊢ Erdos375Prop →
  ∃ c > 0,
    ∀ᶠ (n : ℕ) in atTop, ↑(Nat.nth Nat.Prime (n + 1)) - ↑(Nat.nth Nat.Prime n) < ↑(Nat.nth Nat.Prime n) ^ (1 / 2 - c)
  sorryAll goals completed! 🐙

In particular, if Erdos375Prop is true, then Legendre's conjecture is asymptotically true.

@[category research solved, AMS 11]
theorem erdos_375.variants.legendre : Erdos375Prop →
    (∀ᶠ n in atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p) :=
  fun hp => LegendreConjecture.bounded_gap_legendre (erdos_375.variants.bounded_gap hp)

It is easy to see that for any n ≥ 1 and k ≤ 2, if n + 1, ..., n + k are all composite, then there are distinct primes p₁, ... pₖ such that pᵢ ∣ n + i for all 1 ≤ i ≤ k.

@[category research solved, AMS 11]
theorem erdos_375.variants.le_two : ∀ n ≥ 1, ∀ k ≤ 2, (∀ i < k, ¬ (n + i + 1).Prime) →
    ∃ p : Fin k → ℕ, p.Injective ∧ ∀ i, (p i).Prime ∧ p i ∣ n + i + 1 := by⊢ ∀ n ≥ 1,
  ∀ k ≤ 2,
    (∀ i < k, ¬Nat.Prime (n + i + 1)) → ∃ p, Function.Injective p ∧ ∀ (i : Fin k), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1
  intro n hnn:ℕhn:n ≥ 1⊢ ∀ k ≤ 2,
  (∀ i < k, ¬Nat.Prime (n + i + 1)) → ∃ p, Function.Injective p ∧ ∀ (i : Fin k), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1 kn:ℕhn:n ≥ 1k:ℕ⊢ k ≤ 2 →
  (∀ i < k, ¬Nat.Prime (n + i + 1)) → ∃ p, Function.Injective p ∧ ∀ (i : Fin k), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1 hkn:ℕhn:n ≥ 1k:ℕhk:k ≤ 2⊢ (∀ i < k, ¬Nat.Prime (n + i + 1)) → ∃ p, Function.Injective p ∧ ∀ (i : Fin k), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1
  interval_cases k«0»n:ℕhn:n ≥ 1k:ℕhk:0 ≤ 2⊢ (∀ i < 0, ¬Nat.Prime (n + i + 1)) → ∃ p, Function.Injective p ∧ ∀ (i : Fin 0), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1«1»n:ℕhn:n ≥ 1k:ℕhk:1 ≤ 2⊢ (∀ i < 1, ¬Nat.Prime (n + i + 1)) → ∃ p, Function.Injective p ∧ ∀ (i : Fin 1), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1«2»n:ℕhn:n ≥ 1k:ℕhk:2 ≤ 2⊢ (∀ i < 2, ¬Nat.Prime (n + i + 1)) → ∃ p, Function.Injective p ∧ ∀ (i : Fin 2), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1 <;>«0»n:ℕhn:n ≥ 1k:ℕhk:0 ≤ 2⊢ (∀ i < 0, ¬Nat.Prime (n + i + 1)) → ∃ p, Function.Injective p ∧ ∀ (i : Fin 0), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1«1»n:ℕhn:n ≥ 1k:ℕhk:1 ≤ 2⊢ (∀ i < 1, ¬Nat.Prime (n + i + 1)) → ∃ p, Function.Injective p ∧ ∀ (i : Fin 1), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1«2»n:ℕhn:n ≥ 1k:ℕhk:2 ≤ 2⊢ (∀ i < 2, ¬Nat.Prime (n + i + 1)) → ∃ p, Function.Injective p ∧ ∀ (i : Fin 2), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1 intro h«2»n:ℕhn:n ≥ 1k:ℕhk:2 ≤ 2h:∀ i < 2, ¬Nat.Prime (n + i + 1)⊢ ∃ p, Function.Injective p ∧ ∀ (i : Fin 2), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1
  ·«0»n:ℕhn:n ≥ 1k:ℕhk:0 ≤ 2h:∀ i < 0, ¬Nat.Prime (n + i + 1)⊢ ∃ p, Function.Injective p ∧ ∀ (i : Fin 0), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1 simp_all«0»n:ℕk:ℕhn:1 ≤ n⊢ Function.Injective finZeroElim; intro«0»n:ℕk:ℕhn:1 ≤ na₁✝:Fin 0⊢ ∀ ⦃a₂ : Fin 0⦄, finZeroElim a₁✝ = finZeroElim a₂ → a₁✝ = a₂; grindAll goals completed! 🐙
  ·«1»n:ℕhn:n ≥ 1k:ℕhk:1 ≤ 2h:∀ i < 1, ¬Nat.Prime (n + i + 1)⊢ ∃ p, Function.Injective p ∧ ∀ (i : Fin 1), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1 choose! p hp using (n + 1).exists_prime_and_dvd (byn:ℕhn:n ≥ 1k:ℕhk:1 ≤ 2h:∀ i < 1, ¬Nat.Prime (n + i + 1)⊢ n + 1 ≠ 1 linarithAll goals completed! 🐙)
    exact ⟨fun x => p, fun x => byn:ℕhn:n ≥ 1k:ℕhk:1 ≤ 2h:∀ i < 1, ¬Nat.Prime (n + i + 1)p:ℕhp:Nat.Prime p ∧ p ∣ n + 1x:Fin 1⊢ ∀ ⦃a₂ : Fin 1⦄, (fun x => p) x = (fun x => p) a₂ → x = a₂ grindAll goals completed! 🐙, fun i => byn:ℕhn:n ≥ 1k:ℕhk:1 ≤ 2h:∀ i < 1, ¬Nat.Prime (n + i + 1)p:ℕhp:Nat.Prime p ∧ p ∣ n + 1i:Fin 1⊢ Nat.Prime ((fun x => p) i) ∧ (fun x => p) i ∣ n + ↑i + 1 simpa using hpAll goals completed! 🐙⟩
  ·«2»n:ℕhn:n ≥ 1k:ℕhk:2 ≤ 2h:∀ i < 2, ¬Nat.Prime (n + i + 1)⊢ ∃ p, Function.Injective p ∧ ∀ (i : Fin 2), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1 choose! p hp using (fun i : Fin 2 => (n + i + 1).exists_prime_and_dvd (byn:ℕhn:n ≥ 1k:ℕhk:2 ≤ 2h:∀ i < 2, ¬Nat.Prime (n + i + 1)i:Fin 2⊢ n + ↑i + 1 ≠ 1 linarithAll goals completed! 🐙))
    refine ⟨p, fun x y hxy => ?_, hp⟩«2»n:ℕhn:n ≥ 1k:ℕhk:2 ≤ 2h:∀ i < 2, ¬Nat.Prime (n + i + 1)p:Fin 2 → ℕhp:∀ (i : Fin 2), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1x:Fin 2y:Fin 2hxy:p x = p y⊢ x = y
    by_contra! hr«2»n:ℕhn:n ≥ 1k:ℕhk:2 ≤ 2h:∀ i < 2, ¬Nat.Prime (n + i + 1)p:Fin 2 → ℕhp:∀ (i : Fin 2), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1x:Fin 2y:Fin 2hxy:p x = p yhr:x ≠ y⊢ False
    wlog hq : x < y«2».inrn:ℕhn:n ≥ 1k:ℕhk:2 ≤ 2h:∀ i < 2, ¬Nat.Prime (n + i + 1)p:Fin 2 → ℕhp:∀ (i : Fin 2), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1x:Fin 2y:Fin 2hxy:p x = p yhr:x ≠ ythis:∀ n ≥ 1,
  ∀ (k : ℕ),
    2 ≤ 2 →
      (∀ i < 2, ¬Nat.Prime (n + i + 1)) →
        ∀ (p : Fin 2 → ℕ),
          (∀ (i : Fin 2), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1) → ∀ (x y : Fin 2), p x = p y → x ≠ y → x < y → Falsehq:¬x < y⊢ Falsen:ℕhn:n ≥ 1k:ℕhk:2 ≤ 2h:∀ i < 2, ¬Nat.Prime (n + i + 1)p:Fin 2 → ℕhp:∀ (i : Fin 2), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1x:Fin 2y:Fin 2hxy:p x = p yhr:x ≠ yhq:x < y⊢ False
    ·«2».inrn:ℕhn:n ≥ 1k:ℕhk:2 ≤ 2h:∀ i < 2, ¬Nat.Prime (n + i + 1)p:Fin 2 → ℕhp:∀ (i : Fin 2), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1x:Fin 2y:Fin 2hxy:p x = p yhr:x ≠ ythis:∀ n ≥ 1,
  ∀ (k : ℕ),
    2 ≤ 2 →
      (∀ i < 2, ¬Nat.Prime (n + i + 1)) →
        ∀ (p : Fin 2 → ℕ),
          (∀ (i : Fin 2), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1) → ∀ (x y : Fin 2), p x = p y → x ≠ y → x < y → Falsehq:¬x < y⊢ False exact this n hn k hk h p hp y x hxy.symm hr.symm (byn:ℕhn:n ≥ 1k:ℕhk:2 ≤ 2h:∀ i < 2, ¬Nat.Prime (n + i + 1)p:Fin 2 → ℕhp:∀ (i : Fin 2), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1x:Fin 2y:Fin 2hxy:p x = p yhr:x ≠ ythis:∀ n ≥ 1,
  ∀ (k : ℕ),
    2 ≤ 2 →
      (∀ i < 2, ¬Nat.Prime (n + i + 1)) →
        ∀ (p : Fin 2 → ℕ),
          (∀ (i : Fin 2), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1) → ∀ (x y : Fin 2), p x = p y → x ≠ y → x < y → Falsehq:¬x < y⊢ y < x grindAll goals completed! 🐙)
    ·n:ℕhn:n ≥ 1k:ℕhk:2 ≤ 2h:∀ i < 2, ¬Nat.Prime (n + i + 1)p:Fin 2 → ℕhp:∀ (i : Fin 2), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1x:Fin 2y:Fin 2hxy:p x = p yhr:x ≠ yhq:x < y⊢ False have hy : y = x + 1 := by⊢ ∀ n ≥ 1,
  ∀ k ≤ 2,
    (∀ i < k, ¬Nat.Prime (n + i + 1)) → ∃ p, Function.Injective p ∧ ∀ (i : Fin k), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1 grindAll goals completed! 🐙
      have := hy ▸ Nat.dvd_sub (hp y).2 (hxy ▸ (hp x).2)n:ℕhn:n ≥ 1k:ℕhk:2 ≤ 2h:∀ i < 2, ¬Nat.Prime (n + i + 1)p:Fin 2 → ℕhp:∀ (i : Fin 2), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1x:Fin 2y:Fin 2hxy:p x = p yhr:x ≠ yhq:x < yhy:y = x + 1 := le_two._proof_5 x y hqthis:p (x + 1) ∣ n + ↑(x + 1) + 1 - (n + ↑x + 1) := hy ▸ Nat.dvd_sub (hp y).right (hxy ▸ (hp x).right)⊢ False
      have := (hp 1).1n:ℕhn:n ≥ 1k:ℕhk:2 ≤ 2h:∀ i < 2, ¬Nat.Prime (n + i + 1)p:Fin 2 → ℕhp:∀ (i : Fin 2), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1x:Fin 2y:Fin 2hxy:p x = p yhr:x ≠ yhq:x < yhy:y = x + 1 := le_two._proof_5 x y hqthis✝:p (x + 1) ∣ n + ↑(x + 1) + 1 - (n + ↑x + 1) := hy ▸ Nat.dvd_sub (hp y).right (hxy ▸ (hp x).right)this:Nat.Prime (p 1) := (hp 1).left⊢ False
      simp_all [Nat.not_prime_one]All goals completed! 🐙

There exists a constant c > 0 such that for all n, if k < c * (log n / (log (log n))) ^ 3 → (∀ i < k, ¬ (n + i + 1).Prime), then there are distinct primes p₁, ... pₖ such that pᵢ ∣ n + i for all 1 ≤ i ≤ k. This is proved in [RST75]. There is no need to only consider sufficiently large n because one can always take c small enough so that k < c * (log n / (log (log n))) ^ 3 implies that k = 0 until n is large.

@[category research solved, AMS 11]
theorem declaration uses 'sorry'erdos_375.variants.log : ∃ c > 0, ∀ n k : ℕ,
    k < c * (Real.log n / (Real.log (Real.log n))) ^ 3 → (∀ i < k, ¬ (n + i + 1).Prime) →
    ∃ p : Fin k → ℕ, p.Injective ∧ ∀ i, (p i).Prime ∧ p i ∣ n + i + 1 := by⊢ ∃ c > 0,
  ∀ (n k : ℕ),
    ↑k < c * (Real.log ↑n / Real.log (Real.log ↑n)) ^ 3 →
      (∀ i < k, ¬Nat.Prime (n + i + 1)) → ∃ p, Function.Injective p ∧ ∀ (i : Fin k), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1
  sorryAll goals completed! 🐙


end Erdos375