Are there non-standard counterexamples to the Fermat Last Theorem?

I am going to respond to two questions quoted below, which come from this comment. Here "TP" means "transfer principle". I've switched the order of the questions.

... why it does not prove that any sentence for which TP is preserved and which is true in the standard model, must be true in all models, and hence provable in PA.

Here is an informal summary of how the hyperreal construction works. If we begin with any structure $M$, with an associated formal language, and take an ultrapower, we will obtain a structure $M^*$. By Los's theorem, $M^*$ will satisfy the same sentences as $M$ in that formal language. In the cases of interest, $M$ has an internal real line $\mathbb{R}$ and an internal semiring of naturals $\mathbb{N}$. The ultraproduct $M^*$ with then have an internal "hyperreal" line $\mathbb{R}^*$ and an internal semiring of "hypernaturals" $\mathbb{N}^*$.

If we begin with different models $M_1$ and $M_2$ (e.g. if one of them is nonstandard), we simply obtain different models $M_1^*$ and $M_2^*$. Sentences from the appropriate language are true in $M_1$ if and only if they are true in $M_1^*$, and true in $M_2$ if and only if they are true in $M_2^*$, but if there was no connection between $M_1$ and $M_2$ to begin with then the ultrapower construction can't create one. The transfer principle only holds between each individual model $M$ and its ultrapower $M^*$.

At this point I am most curious as to why a naive transplantation of the TP argument to "nonstandard" embedding does not (indirectly) prove that FLT holds in all models of PA, even if it does not provide any means of (directly) converting Wiles's proof into PA.

The original question is right - "Wiles's proof uses not as much analysis as high end algebraic geometry". This is bad for nonstandard analysis, though, because when we make the hyperreal line we normally begin with a structure $M$ that is just barely more than the field of real numbers. This is good if we want to work with the kinds of constructions used in elementary analysis, but not as useful if we need to work with more general set-theoretic constructions.

Wiles' proof as literally read uses various set-theoretic constructions of "universes". So, to try to approach that in a nonstandard setting, we would want to start with a model $M$ that is much more than just a copy of the real line. That would not seem to help us show that FLT holds in every model of PA.

The thing about the proof is that the "literal" reading is too strong. I am no expert in the algebraic geometry used, but I followed the discussions in several forums, and here is the situation as I understand it. The proof relies on several general lemmas which, to be proved in utmost generality, were proved using very strong methods. However, in concrete cases such as FLT only weaker versions of the lemmas are needed, and experts seem to believe that the weaker versions should be provable in PA. But actually working out the proof would require a lot of effort to prove in PA the special, weaker cases of all the necessary lemmas and then combine them to get FLT.

This is very analogous in my mind to the fact that in logic we often prove things using strong axioms, but experts in logic recognize that these things are also provable, in concrete cases, in much weaker systems. We don't generally dwell on that, or even point it out, unless there is a specific reason. Indeed, the number of things which I know are provable in PA is much larger than the number for which I have ever written out a proof in PA.

Colin McLarty has published several papers on the axioms needed for FLT. You could look at What does it take to prove Fermat's Last Theorem? from the Bulletin of Symbolic Logic which is relatively accessible.

The OP asks "Are there non-standard counterexamples to the Fermat Last Theorem?" The question can actually be interpreted in two different ways since the OP mentioned in a comment that "a copy of non-standard integers is embedded into hyperreals."

If the question is interpreted as applying to all possible models of PA then by the completeness theorem, if Wiles' theorem is not provable in PA then there should be models where the result fails.

If the question is interpreted as applying to models embeddable in the hyperreals, as the OP's comment suggests, then one could note the following. The theorem can be expressed by a first order formula, and so can Wiles' theorem (that there are no solutions). The transfer principle applies to such formulas. Therefore Wiles' theorem remains true over the hyperintegers, as well. Thus there are no nonstandard counterexamples, either.

This point was made in Mike Haskel's answer in a slightly different form but deleted presumably because Mike come to adopt the first interpretation. I am not sure if the OP can see the deleted answer (this depends on the reputation score). The point remains valid with regard to the second interpretation.

Fermat's theorem is expressible in PA. Therefore an elementary extension like Skolem's constructed in 1933 would also satisfy Wiles' theorem since Wiles did prove Fermat's last theorem, even though he used tools that go beyond PA. Therefore this provides an answer to the OP's question, who specifically mentioned the embedding of the nonstandard integers into the hyperreals in his first comment below the question.

With regard to your question as to the foundational status of the proof of FLT, a pretty much up-to-date account can be found here. A key name is McLarty.