Skip to content

Erdős problem 375

Start work

Is Erdos375Prop true?

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

375.lean

Retained formal statement5 of 5

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.

FormalConjectures/ErdosProblems/375.leanErdos375.erdos_375.variants.log4 linesExact file
∃ 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
SolvedStatement only, no proof