[FOM] Candidates for Harvey Friedman's Pi^0_1 formula P(n)

[Timothy Y. Chow]

Harvey Friedman asks for a Pi^0_1 formula P(n) with one free parameter n 
such that for any fixed n, P(n) is of enormous mathematical interest, and
at the same time, for all small n, P(n) can be simulated by a small Turing 
machine.

Of course it seems difficult to find such a formula, but to make the
problem easier, suppose we drop the smallness requirement for a moment,
and also weaken "enormous" to "non-trivial."  Even then it's not so easy,
because we probably want the truth value of P(n) to vary with n in some
complicated way.  If P(n) were true for all n, then my feeling is that
people would be less interested in individual values of n.  Moreover,
Harvey Friedman seems to want the table of truth values to be too complex 
to compress significantly.

The closest candidate that comes to my mind is the calculation of homotopy 
groups of spheres.  There's no known way to calculate pi_(n+k)(S^n) for 
arbitrary n and k, nor to my knowledge is there any conjectured overall
pattern.  (There are some general theorems and general conjectures, of
course, but I don't think they come close to describing even conjecturally
what happens in all cases.)

But here's the question: Is the statement "pi_(n+k)(S^n) = [some specific
group]" equivalent to a Pi^0_1 formula?

There's a theorem of Wu that relates the homotopy groups of S^3 to groups
defined by certain generators and relations; this probably helps one to
"arithmetize" the statement in that case, but I don't know of any such
theorem in general.

Tim