Friedman [1] conjectured


  Every theorem published in the Annals of Mathematics whose
  statement involves only finitary mathematical objects (i.e., what logicians
  call an arithmetical statement) can be proved in EFA. EFA is the weak
  fragment of Peano Arithmetic based on the usual quantifier free axioms for
  0,1,+,x,exp, together with the scheme of induction for all formulas in the
  language all of whose quantifiers are bounded. This has not even been
  carefully established for Peano Arithmetic. It is widely believed to be
  true for Peano Arithmetic, and I think that in every case where a logician
  has taken the time to learn the proofs, that logician also sees how to
  prove the theorem in Peano Arithmetic. However, there are some proofs which
  are very difficult to understand for all but a few people that have
  appeared in the Annals of Mathematics - e.g., Wiles' proof of FLT.


Have there been any serious challenges to this or the weaker conjecture with Peano arithmetic in place of exponential function arithmetic?

[1] http://cs.nyu.edu/pipermail/fom/1999-April/003014.html

To Mark Sapir:

The conjecture says "can be proved in EFA". If it "was not proved in EFA" then that does not count. However, I am still interested if it "was not proved in EFA". Since EFA can still develop some theory of recursive functions, the fact that recursive functions are mentioned, or even used, does not imply that the proof is outside EFA. 

It is also true that EFA is fully capable of proving recursive unsolvability theorems. 

The only proofs we have that given mathematical statements are not provable in EFA is to show that the mathematical statements inherently give rise to functions that are not bounded by any finite height exponential stack. Is this definitely the case here? Or is there a conjecture to that effect? 

Harvey Friedman
