Hi, Wiles's proof of Fermat's last theorem has been pretty much accepted by the experts in his field. His proof, however, uses very powerful techniques in arithmetic algebraic geometry. Is is possible to translate his proof into a strictly Peano arithmetic version, or is this still an open question? Thanks very much, Lucas Wiman