Number theory
Erdős 913 - infinite many 8p sq sub one primes
It is likely that there are infinitely many primes such that is also prime.References
No one has attempted this yet.
Formal statement
Lean type
{p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}.InfiniteWhat you must prove
import FormalConjectures.ErdosProblems.«913»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos913.erdos_913.variants.infinite_many_8p_sq_sub_one_primes" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/913.lean
- Source type SHA-256
- sha256:9238757bf05c18a87aa8fb76bc1cdfaffce9c8331144a35da36765f6bbb3dea5
- Task id
- fc-379fc029-variants-infinite-many-8p-sq-sub-one-primes-c71f024fa8-formalized-v1
- Task commitment
- sha256:4711f386aa788755b10235084ac2244a4340db678b94dd4c5e33632c6e188353
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.