1) Is EFA stronger than recursive algorithm? (This can be in term of proof theoretic ordinal, or whatsoever - to rephrase the question, are all problems that can be solved(and halt) by recursive algorithm expressible in EFA?
2) Is Friedman's grand conjecture proven?
3) Is it proven that there cannot be an algorithm that receives the proof that is not expressed in EFA form as an input and outputs a proof in EFA (for problems that have proofs expressible in EFA)?