Number theory · Last catalog review 26 Jul 2026
Erdős Problem 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 , where the conjecture is trivially false.]References
Published 1 Aug 2026Never attempted
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 < PWhat 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-e923379e-erdos779-erdos-779-181ee51c3f-formalized-v1
- Task commitment
- sha256:facf3709140652c73454bda021c127403068eb3d648fd293df27501b091ae487
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.