Is Fermat's last theorem provable in Peano arithmetic?

Question

The sentence $S$ which Gödel in his proof of the incompleteness theorem proves to be be unprovable in the system of Peano arithmetic can be proved (as a true theorem of PA) outside PA (and necessarily only outside PA).

Compared to Fermat's last theorem $F$ which states that for $n>2, a, b, c \in \mathbb{N}$

$$a^n + b^n = c^n \rightarrow a = 0 \text{ or } b = 0$$

it's hard to write $S$ down as a sentence of PA and understand its meaning. Nevertheless it's a (true) theorem of pure number theory, perfectly expressible in the language of PA. And for both $S$ and $F$ no proof inside PA is known. (For $S$ there cannot be one.)

My question is: Can it be shown (and/or how can be shown) that Fermat's last theorem has no proof in the language of Peano arithmetic?

This would imply that one must leave the realm of Peano arithmetic to prove it. As a side question: How would one - in general terms - name the realms in which Gödel and Wiles performed their proofs? "Model theory" and "algebraic geometry"?

Answer 1

This paper shows that Fermat's Last Theorem (FLT) is not provable in weak arithmetics, including theories where exponentiation is not definable from addition and multiplication; in particular, FLT is not provable in Presburger artithmetic extended with a natural set of axioms for exponentials.

Concerning Peano arithmetic (PA), as far as I know, there is no negative result and the problem is still open. Actually, one of the main issues whether the proof of FLT can be formalized in PA is that it relies on higher-order structures and a priori there is no evidence that they can be reformulated in first-order language of PA. Moreover, even if all the necessary concepts can be stated in the first-order language of PA, Wiles' original proof of FLT uses set-theoretical assumptions unprovable in Zermelo-Fraenkel set theory with axiom of choice (ZFC, which is stronger than PA) and there is no a priori guarantee that we do not need axioms with greater strength than PA.

However, McLarty in this paper claims that in the proof of FLT:

[...] certainly much less than ZFC is used in principle, probably nothing beyond PA, and perhaps much less than that. [p. 359]

Macintyre in the appendix of his chapter of the book Kurt Gödel and the Foundations of Mathematics: Horizons of Truth proposed and sketched a project of formalizing Wiles's proof of FLT in Peano arithmetic. He says:

There is no possibility of giving a detailed account in a few pages. I hope nevertheless that the present account will convince all except professional skeptics that [the modularity theorem, which plays a key role in Wiles' proof] is really $\Pi^0_1$ [p. 15].