[FOM] Difficult?

[Lucas Wiman]

 > This still does not answer the original question about hardness. A
 > hardness result would probably be quite difficult to show as it would
 > effectively imply that there is no poly-time algorithm for computing 
f(n).

Unless I'm misunderstanding you, then the question of poly-time 
algorithm for calculating pi(n) mod 2 is not relevant to Friedman's 
question about how many symbols this calculation would take in ZFC.  
There is, for example, a poly-time algorithm for determining whether 
Mersenne numbers are prime (either Agrawal et al's recent algorithm or 
the more classical Lucas-Lehmer test).  Yet we have no reason (to my 
knowledge) to suspect that if 2^(2^127-1)-1 is prime, then it would 
require fewer than 2^100 symbols to prove it in ZFC.  Even a linear time 
algorithm would require O(2^127) symbols to do it.

(Aside:  The primality of this "double Mersenne prime" has been looked 
at, and to my knowledge no factor is known of it.  The reason it was 
looked at is as follows:
2 is prime
3=2^2-1 is prime
7=2^3-1 is prime
127=2^7-1 is prime
2^127-1 is prime
2^(2^127-1)-1 must be prime too, right?)

- Lucas Wiman