Skip to content

Erdős problem 779

Start work

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

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

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=0n = 0, where the conjecture is trivially false.]

FormalConjectures/ErdosProblems/779.leanErdos779.erdos_7793 linesExact file
∀ n ≥ 1,  have P := ∏ i ∈ Finset.range (n + 1), Nat.nth Nat.Prime i;  ∃ p, Nat.Prime p ∧ Nat.Prime (P + p) ∧ Nat.nth Nat.Prime n < p ∧ p < P
OpenStatement only, no proof