Number theory
Erdős 218 - infinite equal prime gap
There are infintely many indices such that the prime gap at is equal to the prime gap at . This is equivalent to the existence of infinitely many arithmetic progressions of length , seeerdos_141.variants.infinite_three.
References
No one has attempted this yet.
Formal statement
Lean type
{n | primeGap n = primeGap (n + 1)}.InfiniteWhat you must prove
import FormalConjectures.ErdosProblems.«218»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos218.erdos_218.variants.infinite_equal_prime_gap" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/218.lean
- Source type SHA-256
- sha256:e0580853f98f842ebfd4cca33ecdcb3dd6b3e76b0df71f00bc687b73e9f7f056
- Task id
- fc-379fc029-variants-infinite-equal-prime-gap-b79aee4163-formalized-v1
- Task commitment
- sha256:20e0f838a39f365afb4aa9cc9540c907b5c91619039a42a62162f18aff2b2c48
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.