[FOM] Difficult?

[Harvey Friedman]

Let n be a specific big integer of some interest. I want to know if 
the number of primes less than n is even or odd.

DIGRESSION. Is the set of all positive integers n in base 2 such that 
the number of primes less than n is even, #P-complete in the sense of 
computational complexity theory? Same question with regard to the 
function f(n) = the number of primes less than n.

So here is the main event.

CONJECTURE. "the number of primes less than 2^2^2^2^2^2^2^2 is even" 
cannot be proved or refuted in ZFC even with large cardinal axioms, 
without using at least 2^2^100 symbols, even if abbreviations are 
allowed.