Let $n > 1$ and $p_{1} < \dots < p_{n}$ denote the first $n$ primes. Let $P = \prod_{1 \leq i \leq n} p_{i}$ . Does there always exist some prime $p$ with $p_{n} < p < P$ such that $P + p$ is prime?

Worked, still open.

number theory · open · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

It is recorded as an Erdős problem (attributed to **Deaconescu**) and is currently listed as **“Open, but could be disproved with a finite counterexample.”** ([Erdős Problems][1]) In particular, the Erdős-problems site notes that **Deaconescu verified the statement computationally for (n\le 1000)**, and that Erdős expe…

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 11 · open (literature)

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

formal-conjectures/779.lean ↗

oeis

A005235 — Fortunate numbers: least m > 1 such that m + prime(n)# is prime, where p# denotes the product of all primes <= p.3,5,7,13,23,17,19,23,37,61,67,61,71,47,107,59,61,109,89,103,79,151,197,101,103,233,223,127,223,191,163,229,643,239,157,1

status

open

evidence

formal

oeis

status

Search Vela