FOM: Eliminability of "Analytic" methods in number theory

[JOE SHIPMAN, BLOOMBERG/ NEW YORK]

Two questions for you, Steve:
 1) What "big theorems" of number theory have actually been proved without
going beyond the methods you reduce to PRA or PA?  Can Wiles's theorem be so
proved?  Faltings's theorem?  Goldfeld's result on the zeroes of the Riemann
zeta function?  The result that every sufficiently large even number is the sum
of a prime and the product of two primes?
 2) What kind of blowup is there in length of proof in your reductions?
-- Joe Shipman