ErdosProblems · research open · AMS 11
unsolvedsorry — nobody on it
Erdős Problem 779
Conjecture 779 · Erdős
The formal statement below is all there is.
Formal statement · Lean 4.lean
theorem erdos_779 (n : ℕ) (hn : n ≥ 1): let P := ∏ i ∈ range (n + 1), nth Nat.Prime i
∃ p, p.Prime ∧ (P + p).Prime ∧ nth Nat.Prime n < p ∧ p < P := by
sorryProof. sorry
Nobody has tried yet.