Erdős problem 779 · problems.science

A Conjecture of Marian Deaconescu, see p.120 in https://doi.org/10.2307/2975810

Sources

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

1 retained statement2415f78e850a

FormalConjectures/ErdosProblems/

779.lean

Retained formal statement1 of 1

A Conjecture of Marian Deaconescu, see p.120 in https://doi.org/10.2307/2975810

[Needed to index shift in order to avoid trivial case $n = 0$ , where the conjecture is trivially false.]

FormalConjectures/ErdosProblems/779.leanErdos779.erdos_7793 linesExact file

1∀ n ≥ 1,2  have P := ∏ i ∈ Finset.range (n + 1), Nat.nth Nat.Prime i;3  ∃ p, Nat.Prime p ∧ Nat.Prime (P + p) ∧ Nat.nth Nat.Prime n < p ∧ p < P

OpenStatement only, no proof