Number theory
Erdős 17
**Erdős Problem 17.** Are there infinitely many cluster primes?References
No one has attempted this yet.
Formal statement
Lean type
True ↔ {p | Erdos17.IsClusterPrime p}.InfiniteWhat you must prove
import FormalConjectures.ErdosProblems.«17»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos17.erdos_17" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/17.lean
- Source type SHA-256
- sha256:4e4edda55e193af3b1e6e72381cf8a97a4eb48adfddf96bec2b8bcca7bfc9eab
- Task id
- fc-379fc029-erdos17-erdos-17-69d191880f-formalized-v1
- Task commitment
- sha256:f490dd6da820e203b881fe71d64c3e5acfe1d33df1202545b80e55af56edaeef
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.