Number theory
Erdős 1209 - part iii d
Are there such that is infinitely often squarefree?References
- [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.
No one has attempted this yet.
Formal statement
Lean type
True ↔ ∃ n, {k | Squarefree (n + 2 ^ 2 ^ k)}.InfiniteWhat you must prove
import FormalConjectures.ErdosProblems.«1209»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos1209.erdos_1209.parts.iii.d" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/1209.lean
- Source type SHA-256
- sha256:e789aec3354065553035a6104a2473dbd2bc783e54f06ab500b85ab7b944a37a
- Task id
- fc-379fc029-iii-d-e45f68a943-formalized-v1
- Task commitment
- sha256:686d66120a12f72cb77ba5d67ac73c4a14518e29aebdbcbf9dd39b540ddd98ff
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.