Formal target: Corpus.Erdos10.erdos_10.variants.granville_soundararajan_odd
Granville and Soundararajan [GrSo98] have conjectured that at most $3$ powers of $2$ suffice for all odd integers, and hence at most $4$ powers of $2$ suffice for all even integers.
Exact formal statement
And (LE.le.{0} (Set.ofPred.{0} fun n => And (Odd.{0} n) (LT.lt.{0} 1 n)) (Corpus.Erdos10.sumPrimeAndTwoPows 3))
(LE.le.{0} (Set.ofPred.{0} fun n => And (Even.{0} n) (Ne.{1} n 0)) (Corpus.Erdos10.sumPrimeAndTwoPows 4))This target is a formal statement, not a proof of the problem.
Environment availability: available.