Combinatorics
Erdős 10 - grechuk
Bogdan Grechuk has observed that is not the sum of a prime and at most powers of , and pointed out that parity considerations, coupled with the fact that there are many integers not the sum of a prime and powers of suggest that there exist infinitely many even integers which are not the sum of a prime and at most powers of ).References
No one has attempted this yet.
Formal statement
Lean type
({n | Even n} \ Erdos10.sumPrimeAndTwoPows 3).InfiniteWhat you must prove
import FormalConjectures.ErdosProblems.«10»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos10.erdos_10.variants.grechuk" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/10.lean
- Source type SHA-256
- sha256:b92788d3cc0d75ad145bb34985748e1cb9d91b0df6880bf7c63452f123611241
- Task id
- fc-379fc029-variants-grechuk-e26c885566-formalized-v1
- Task commitment
- sha256:75dae50947998fe526401998132fe589b236a539908bc9166e8f2b05d8a8f28f
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.