Erdős problem 375 · problems.science

Is Erdos375Prop true?

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

375.lean

Retained formal statement3 of 5

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.

FormalConjectures/ErdosProblems/375.leanErdos375.erdos_375.variants.le_two3 linesExact file

1∀ n ≥ 1,2  ∀ k ≤ 2,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

Sources

Search problems.science