All open problems
Source labels openChecked July 26, 2026
Erdős Problem 913: Infinite Many 8p Sq Add One Primes
It is likely that there are infinitely many primes such that is also prime.
Mathematical statement
It is likely that there are infinitely many primes such that is also prime.
Statement source: Erdős Problems statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
erdos_913.variants.infinite_many_8p_sq_add_one_primes
Complete statement target, proof intentionally absentLean 4
theorem erdos_913.variants.infinite_many_8p_sq_add_one_primes : { p | p.Prime ∧ (8 * p ^ 2 - 1).Prime }.Infinite := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References