# Does Fermat hold in non-standard models?

Let $n \geq 3$ be a natural number and $PA$ denote Peano arithmetic. Do we have

$PA \models \forall x,y,z \geq 1 : x^n + y^n \neq z^n$?

In other words, does Fermat's Last Theorem hold also in non-standard models of the natural numbers?

If this problem is open, what is its current state of progress?

-
I think this is still an open problem. I heard that Angus Macintyre has a draft proof of FLT in PA, but I don't know the current status of the draft. –  François G. Dorais Sep 18 '10 at 19:29
There is relevent discussion at mathoverflow.net/questions/35746/… on what Wiles' proof uses. –  Joel David Hamkins Sep 18 '10 at 19:30
@Joel: Yes I saw this discussion, but I think it touches only the subject of inaccessible cardinals, and justufies the proof in $\mathbb{N}$. But of course, I have no idea about the details of Wiles' proof. –  Martin Brandenburg Sep 19 '10 at 8:46
Some related thing: <<To my mind, the highlight of this period of building recursive models for the purposes of independence results was the results of the early 1960s by Shepherdson, who, using algebraic methods, produced beautiful nonstandard models of quantifier-free arithmetic in which he showed number theoretic results such as the infinitude of primes and Fermat's Last Theorem (in fact, for exponent 3) are false.>> The quote is from Kaye's paper "Tennenbaum's theorem for models of arithmetic". – Sergei Tropanets 0 secs ago –  Sergei Tropanets Sep 20 '10 at 23:02
Is there any news about Macintyre's proof? –  Hans Stricker Jan 20 '11 at 9:03