Conjectures.io

Number theory

Erdős 779

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.]

References

No one has attempted this yet.

Formal statement

Lean type

∀ 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

What you must prove

import FormalConjectures.ErdosProblems.«779»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos779.erdos_779" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/779.lean

Source type SHA-256
sha256:f13a12045cd1f1888471e8756e655df3bac90224417103255c7625d7410d5669
Task id
fc-379fc029-erdos779-erdos-779-de8ea9f48f-formalized-v1
Task commitment
sha256:d659f50ea49a0f4fa7de9002689fd56b48adcfa84c3b4e9cb8f5c91db9dd9196

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.