[FOM] What is the current state of the research about proving FLT?

[Harvey Friedman]

On Sun, Jan 7, 2018 at 3:00 PM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:
> Consider some "easy" proof such as the irrationality of sqrt(2).  If we were
> to formalize this proof in some axiomatic system S and then were to discover
> that S is inconsistent, then we would simply shrug and discard S. The
> inconsistency of S would not affect our belief in the correctness of the
> proof that sqrt(2) is irrational.  We would just come up with some other
> system S' in which we could formalize the proof.  And if S' turns out to be
> inconsistent, we would come up with S''.  Throughout, our certainty in the
> correctness of the proof of the irrationality of sqrt(2) would remain
> unmoved.
>
I am not convinced by this line of reasoning. The key possibility is
that after seeing such (extremely unlikely, by the way) fundamental
inconsistencies, people will also try to prove 1 = 0 using the same
kind of arguments that were used to prove the irrationality of
sqrt(2). Or at least related totally accepted mathematical theorems.
If these are enough of the same kind of arguments, then indeed there
would be a revolutionary collapse of maybe the very idea that
mathematics can legitimately get even close to any kind of infinities.

If one tries to be precise about just what these imaginary
possibilities are, one gets into the issue of just how one wants to
formalize the proof of the irrationality of sqrt(2), and armed with
the inconsistency in it, see exactly what range of formal systems this
inconsistency must transfer over to.

A related example of such a thing is that some mathematicians claim to
be actually unconvinced that PA is consistent. Although there is
absolutely no evidence or hint of any such problem with PA, I am
perfectly happy to consider the possibility that PA is inconsistent -
but only because I am interested in the research that this suggests.

In extremely pared down fundamental systems for SRM = strict reverse
mathematics, one proves that the Bolzano -Weierstrass theorem and many
related theorems imply that each PA_n is consistent. Also PA is
interpretable in BW plus tiny SRM. Of course, this is well known if
you use my RCA_0 (and some standard subsystems). But the fact that
tiny SRM is enough makes it difficult to imagine Chow's "shrug and
discard". I.e., the imaginary inconsistency in PA gets converted to a
refutation of BW in tiny SRM.

There is an ambitious project under way, as far as I know, to get a
computer verification of the Classification of Finite Simple Groups.
Tools are being built for this mammoth project, and a motivating idea
is that without this, the proof could disappear from humanity given
its size and given that the incentive for people to become expert
enough to see the whole proof is diminishing to zero.

At this point, I have not heard of any serious plan to get a computer
verification of FLT or even simpler sophisticated things. I am under
the impression that when serious abstract machinery is involved, the
computer verification gets a lot harder. It would be nice to get
Jeremy Avigad's take on this and the previous paragraph.

Harvey Friedman