Number theory axioms

Steve Landsburg writes:

However, we still don’t know whether Fermat’s Last Theorem follows from the standard axioms for arithmetic.

Colin Mclarty says that the big modern cohomological number theory theorems, including Fermat’s Last Theorem, were all proved using Grothendieck’s tools, making use of an axiom stronger than Zermelo–Fraenkel set theory (ZFC). He says that there is a belief that these theorems can be proved in ZFC, but no one has done it.

Usually, mathematicians only agree that a theorem has been proved if it has been proved in ZFC. It seems to me that someone should prove that Grothendieck's work and its consequences is provable in ZFC.

Update: NewScientist reports:

To complete his proof, Wiles assumed the existence of a type of large cardinal known as an inaccessible cardinal, technically overstepping the bounds of conventional arithmetic. But there is a general consensus among mathematicians that this was just a convenient short cut rather than a logical necessity. With a little work, Wiles's proof should be translatable into Peano arithmetic or some slight extension of it.

The article says that large cardinals are needed to decide other arithmetic statements.