FOM: a "hard" problem?

[Harvey Friedman]

PROBLEM: Is the number of primes less than 2^100 even? Is the number of
primes less than 2^10,000 even?

I am under the impression that such problems are completely hopeless, even
with the aid of a computer. Hopeless, even if we wish to prove or refute it
with a high degree of certainty. Hopeless even to justify making a
conjecture as to whether it is true or false.

But should we conjecture some sort of formal undecidability of this
question? E.g.,

CONJECTURE?? The version with 2^10,000 cannot be proved or refuted in ZFC
with abbreviations without using more than 2^100 bits.

This leads us to the question of what the best example is of a problem like
this where such a conjecture can be verified?

At the moment, the examples I can think of are hopelessly obnoxious.