As far as I know, whether Fermat's Last Theorem is provable in Peano Arithmetic is an open problem. What is known about this problem?


In particular, what is known about the arithmetic systems $PA + \text{Fermat's Last Theorem}$ and $PA + \lnot \text{Fermat's Last Theorem}$?


Note in particular that if $PA \vdash \text{Fermat's Last Theorem}$, the first system will just be $PA$ and the second system with be inconsistent. If FLT is independent of PA, then both will be consistient systems distinct from $PA$. $PA \vdash \lnot \text{Fermat's Last Theorem}$ is not possible, since $PA$ and Fermat's last theorem are both true in $\mathbb N$.



What is known about the relationship between Fermat's last theorem and Peano Arithmetic?
The main reference for this topic is Angus Macintyre's appendix to Chapter 1 ("The Impact of Gödel's Incompleteness Theorems on Mathematics") of *Kurt Gödel and the Foundations of Mathematics: Horizons of Truth* (Cambridge University Press, 2011).


There are a a couple of reasons why one might wonder whether the proof of FLT can be formalized in PA. 


1. The modularity theorem, as well as various arguments in the proof of the modularity theorem, appears at first glance to quantify over higher-order structures (sets of integers, sets of sets of integers, etc.), and so one might wonder whether all the necessary concepts can even be *stated* in the first-order language of arithmetic.
2. Even if the modularity theorem and all other crucial intermediate statements along the way to FLT can be formulated arithmetically, there is no *a priori* guarantee that we don't need to appeal to axioms with greater logical strength than PA.


The "mathematician in the street" is typically more worried about #2. After all, doesn't the proof of FLT use all kinds of fancy-shmancy high-powered mathematics, and isn't PA "elementary"? Maybe one needs powerful axioms to carry out all those "advanced" arguments. While this is a theoretical possibility, there isn't any hint in the proof of FLT that strong axioms are needed. Experts can "smell" the intrusion of a strong axiom from a long way off; for example, the primary reason that the Robertson–Seymour graph minor theorem requires more than PA is that it invokes a highly sophisticated argument by induction at a crucial point. The proof of FLT doesn't give off this sort of odor anywhere. Of course, a smell test is not a proof, but the smart money is that if we run into difficulties trying to prove FLT in PA, it won't be because we need some strong arithmetic axiom. For more on this topic, especially the oft-discussed axiom of universes, see [Colin McLarty's 2010 paper](https://projecteuclid.org/download/pdf_1/euclid.bsl/1286284558) in the *Bulletin of Symbolic Logic* as well as his more recent [arXiv preprint](https://arxiv.org/abs/1102.1773v4).


Issue #1, of whether all the higher-order apparatus in which the proof of FLT is couched is intrinsically necessary, is what Macintyre mainly concerns himself with. His appendix is essentially a ten-page sketch of an argument that all the relevant concepts and intermediate results on the road towards proving FLT can be replaced by "finite approximations" using standard techniques. As Macintyre 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] is really $\Pi\_0^1$.
> 
> 
> 


In short, to say that it is an "open problem" whether FLT is provable in PA, while technically correct, is somewhat misleading. Demonstrating in full detail that FLT is a theorem of PA is more akin to an engineering project, where we more or less know how to proceed and are pretty sure—though of course not mathematically certain—that the project can be carried out if we just work hard enough at it.


