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](http://www.math.ohio-state.edu/~friedman/pdf/GodelLect060202.pdf). 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>



Status of Harvey Friedman's grand conjecture?
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


