This is another way to ask if Wiles's proof can be converted into a "purely number-theoretic" one. If there is no proof in Peano Arithmetic then there should be non-standard integers that satisfy the Fermat equation. I vaguely remember that most proofs in analytic number theory are known to be convertible into elementary ones, probably because some version of predicative analysis is a conservative extension of arithmetic. But Wiles's proof uses not as much analysis as high end algebraic geometry, so I am not sure. Is it convertible into elementary arithmetic, is that even known?

  • 2
    $\begingroup$ @MikeHaskel: That is the interpretation that would make the question make the most sense, but the inclusion of the nonstandard-analysis tag makes me unsure. $\endgroup$ Jul 28, 2016 at 3:08
  • 2
    $\begingroup$ @Eric Yes, that is what I meant. I think a copy of non-standard integers is embedded into hyperreals, hence the tag. $\endgroup$
    – Conifold
    Jul 28, 2016 at 3:13
  • 3
    $\begingroup$ I think of non-standard model of arithmetic as model of "true" arithmetic, in which case there can be no non-standard counterexamples. $\endgroup$ Jul 28, 2016 at 3:15
  • 5
    $\begingroup$ As far as I know this is still an open question (see mathoverflow.net/questions/39239/…, for instance). But my understanding is that experts strongly suspect the proof can be done in PA, just no one has actually undertaken to work out all the details. $\endgroup$ Jul 28, 2016 at 3:18
  • 8
    $\begingroup$ A recent (2016) paper by Glivicky and Kala constructs a model of Presburger arithmetic in which Fermat's Last Theorem fails (counterexamples exist). $\endgroup$
    – hardmath
    Jul 28, 2016 at 3:18

2 Answers 2


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.

  • $\begingroup$ Thanks, Carl. Could you add some preamble and reference to Mikhail's answer at the top of yours, because it is not clear what "it" or "TP argument" refers to in the quotes, and the context is buried at the bottom of a long comment thread under it. $\endgroup$
    – Conifold
    Aug 13, 2016 at 20:32
  • $\begingroup$ No problen, I added a link to the comment, which should help people find it $\endgroup$ Aug 13, 2016 at 21:09

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.

  • 5
    $\begingroup$ I think it's clear from their focus on $PA$ that the OP is not just referring to the hyperintegers, but rather any nonstandard model of $PA$; and for such the question is much more complicated. $\endgroup$ Aug 1, 2016 at 15:51
  • 2
    $\begingroup$ @Mikhail Katz: if we take any model of PA, which may be nonstandard, we can naturally extend it to a model of $\mathsf{ACA}_0$, which is a weakish system of second-order arithmetic that is able to define the real line (relative to the original model of PA). If we then take the usual ultraproduct of that model of $\mathsf{ACA}_0$, with respect to a nonstandard ultrafilter, we obtain a version of the hyperreals which embeds the original model of PA just as the standard hyperreals embed $\omega$. What in the normal ultraproduct construction that requires starting with the standard model of PA? $\endgroup$ Aug 9, 2016 at 19:58
  • 2
    $\begingroup$ There has been a lot of work on nonstandard analogues of subsystems of second order arithmetic recently, actually. To name a few people, one could look for work by Keita Yokoyama, Sam Sanders, or Jerome Keisler. I am sure I am leaving out other important work here; these are just three I know have published in the area. $\endgroup$ Aug 9, 2016 at 20:05
  • 2
    $\begingroup$ @Mikhail Katz: no, but that is irrelevant to the construction, which can be carried out in ZFC just like the construction of the standard hyperreals. We can take the ultraproduct of any structure with itself. If our original structure has its own internal notion of a real line (possibly nonstandard) then the ultraproduct will have its own internal version of a hyperreal line (again possibly nonstandard). Los' theorem applies to all ultraproducts, so we will have a transfer principle, exactly analogous to the usual hyperreals. Every model of $\mathsf{ACA}_0$ has a robust internal real line. $\endgroup$ Aug 10, 2016 at 12:01
  • 2
    $\begingroup$ @Mikhail Katz: The same usual ultrapower construction works. If $N$ is a number in the ground model ($N$ can be standard or nonstandard) and $S = (S_m : m \in \omega)$ is a set in the ultraproduct, where as usual each $S_m$ is a set in the ground model, then we have $N^* \in S$ if and only if $\{ m : N \in S_m \}$ is in the ultrafilter on $\omega$. The ground model has both a collection of "numbers" and a collection of "sets" of "numbers"; this is why we convert the model of PA to a model of $\text{ACA}_0$ before the ultrapower. The ultrapower uses an ultrafilter on the standard $\omega$. $\endgroup$ Aug 11, 2016 at 11:13

Not the answer you're looking for? Browse other questions tagged or ask your own question.