Why the Proof of Fermat’s Last Theorem Doesn’t Need to Be Enhanced

Last June 23 marked the 25th anniversary of the electrifying announcement by Andrew Wiles that he had proved Fermat’s Last Theorem, solving a 350-year-old problem, the most famous in mathematics. The lore surrounding Wiles’ proof — the seven years he worked on the problem in secret, the gap in the proof that appeared a few months after the June announcement, the elegant solution a year later in a joint paper Wiles wrote with his former student Richard Taylor, and his knighthood in 2000 — has entered the annals of mathematical legend.

After Wiles’ breakthrough, it became common to hear talk of a new “golden age” of mathematics, especially in number theory, the field in which the Fermat problem belongs. The methods introduced by Wiles and Taylor are now part of the toolkit of number theorists, who consider the FLT story closed. But number theorists were not the only ones electrified by this story.

I was reminded of this unexpectedly in 2017 when, in the space of a few days, two logicians, speaking on two continents, alluded to ways of enhancing the proof of FLT — and reported how surprised some of their colleagues were that number theorists showed no interest in their ideas.

The logicians spoke the languages of their respective specialties — set theory and theoretical computer science — in expressing these ideas. The suggestions they made were intrinsically valid and may someday give rise to new questions no less interesting than Fermat’s. Yet it was immediately clear to me that these questions are largely irrelevant to number theorists, and any suggestion that it might be otherwise reflects a deep misunderstanding of the nature of Wiles’ proof and of the goals of number theory as a whole.

The roots of this misunderstanding can be found in the simplicity of FLT’s statement, which is responsible for much of its appeal: If n is any positive integer greater than 2, then it is impossible to find three positive numbers a, b and c such that

aⁿ + bⁿ = cⁿ

This sharply contrasts with what happens when n equals 2: Everyone who has studied Euclidean geometry will remember that 3² + 4² = 5², that 5² + 12² = 13², and so on (the list is infinite). Over the last few centuries, mathematicians repeatedly tried to explain this contrast, failing each time but leaving entire branches of mathematics in their wake. These branches include large areas of the modern number theory that Wiles drew on for his successful solution, as well as many of the fundamental ideas in every part of science touched by mathematics. Yet no one before Wiles could substantiate Fermat’s original claim.

The computer scientist had recently been excited to learn about progress in automated proof verification, an ambitious attempt to implement the formalist approach to mathematics in practice. For formalists, a mathematical proof is a list of statements that meet strict requirements:

1. The statements at the top of the list must involve only notions that are universally accepted. In the strictest interpretation, these are limited to the axioms of formal set theory, typically the formal system known as ZFC — shorthand for “Zermelo-Fraenkel, plus choice.” This is totally impractical, so we are also allowed to include theorems that have already been proved — for example, FLT for n = 4, which Fermat himself already proved in the 17th century.
2. Each statement must be obtained by applying the rules of logical deduction to the preceding statements.
3. Finally, the proved theorem should show up as the last statement on the list.

Mathematical logic was developed with the hope of placing mathematics on firm foundations — as an axiomatic system, free of contradiction, that could keep reasoning from slipping into incoherence. Although Kurt Gödel’s work revealed this hope to be chimerical, many philosophers of mathematics, as well as some logicians (a small but vocal minority, according to the set theorist), still regard ZFC and the requirements listed above as a kind of constitution for mathematics.

Mathematicians never write proofs this way, however. A logical analysis of Wiles’ proof points to many steps that appear to disregard ZFC, and this is potentially scandalous: When mathematicians make up rules without checking their constitutionality, how can they know that everyone means the same thing?

Automated proof verification seems to offer a solution. It entails reformulating the proof as a series of discrete statements, each written in an unambiguous language that can be read by a computer, which then confirms that every step deserves to be stamped with a constitutional certification. This painstaking method has been applied with success to many long and difficult proofs, most famously by Thomas Hales and his collaborators to the proof of the Kepler conjecture on the densest way to pack spheres. Verification of Wiles’ proof in particular has long been seen as a major goal. So my computer scientist friend was sincerely disappointed that his search for “pure mathematicians who are unabashedly supportive of the use of automated tools in the construction of their arguments,” as he put it, had so far come up short.

The first thing this disappointment fails to take into account is that Wiles’ proof, complicated as it is, has a simple underlying structure that is easy to convey to a lay audience. Suppose that, contrary to Fermat’s claim, there is a triple of positive integers a, b, c such that

(A)                   a^p + b^p = c^p

for some odd prime number p (it’s enough to consider prime exponents). In 1985, Gerhard Frey pointed out that a, b and c could be rearranged into

(B)       a new equation, called an elliptic curve,

with properties that were universally expected to be impossible. More precisely, it had long been known how to leverage such an elliptic curve into

(C) a Galois representation,

which is an infinite collection of equations that are related to the elliptic curve, and to each other, by precise rules.

The links between these three steps were all well-understood in 1985. By that year, most number theorists were convinced — though proof would have to wait — that every Galois representation could be assigned, again by a precise rule,

(D) a modular form,

which is a kind of two-dimensional generalization of the familiar sine and cosine functions from trigonometry.

The final link was provided when Ken Ribet confirmed a suggestion by Jean-Pierre Serre that the properties of the modular form entailed by the form of Frey’s elliptic curve implied the existence of

(E) another modular form, this one of weight 2 and level 2.

But there are no such forms. Therefore there is no modular form (D), no Galois representation (C), no equation (B), and no solution (A).

The only thing left to do was to establish the missing link between (C) and (D), which mathematicians call the modularity conjecture.

This missing link was the object of Wiles’ seven-year quest. It’s hard from our present vantage point to appreciate the audacity of his venture. Twenty years after Yutaka Taniyama and Goro Shimura, in the 1950s, first intimated the link between (B) and (D), via (C), mathematicians had grown convinced that this must be right. This was the hope expressed in a widely read paper by André Weil, which fit perfectly within the wildly influential Langlands program, named after the Canadian mathematician Robert P. Langlands. The connection was simply too good not to be true. But the modularity conjecture itself looked completely out of reach. Objects of type (C) and (D) were just too different.

The computer scientist left it unclear whether his disappointment with number theorists’ indifference to proof verification was limited to the crucial link between (C) and (D), or whether it encompassed the whole strategy from (A) to (E). I will not try to untangle this ambiguity. But if what the logicians had in mind was to formally verify the published proof of the relation between (C) and (D), then they were setting their sights too low. For one thing, Wiles only proved (a bit more than) enough of the modularity conjecture to complete the (A) to (E) deduction. The complete modularity conjecture was established a few years later by Christophe Breuil, Brian Conrad, Fred Diamond and Richard Taylor. This in no way reflects badly on Wiles’ paper! On the contrary, the fact that so many of the world’s leading number theorists applied themselves to superseding Wiles’ paper within months of seeing it is proof of its richness.

More recently, in the fall of 2016, for example, 10 mathematicians gathered at the Institute for Advanced Study in Princeton, New Jersey, in a successful effort to prove a connection between elliptic curves and modular forms in a new setting. They had all followed different routes to understanding the structure of Wiles’ proof, which appeared when some of them were still small children. If asked to reproduce the proof as a sequence of logical deductions, they would undoubtedly have come up with 10 different versions. Each one would resemble the (A) to (E) outline above, but would be much more finely grained.

Nevertheless — and this is what is missing from the standard philosophical account of proof — each of the 10 would readily refer to their own proof as Wiles’ proof. They would refer in a similar way to the proofs they studied in the expository articles or in the graduate courses they taught or attended. And though each of the 10 would have left out some details, they would all be right.

What kind of thing is Wiles’ proof, if it comes in so many different flavors? In philosophy of mathematics it’s customary to treat a published proof as an approximation of an ideal formalized proof, capable in principle of being verified by a computer applying the rules of the formal system. Nothing outside the formal system is allowed to contaminate the ideal proof — as if every law had to carry a watermark confirming its constitutional justification.

But this attitude runs deeply counter to what mathematicians themselves say about their proofs. Mathematics imposes no ideological or philosophical litmus test, but I’m convinced that most of my colleagues agree with the late Sir Michael Atiyah, who claimed that a proof is “an ultimate check — but it isn’t the primary thing at all.” Certainly the published proof isn’t the primary thing.

Wiles and the number theorists who refined and extended his ideas undoubtedly didn’t anticipate the recent suggestions from the two logicians. But — unlike many who follow number theory at a distance — they were certainly aware that a proof like the one Wiles published is not meant to be treated as a self-contained artifact. On the contrary, Wiles’ proof is the point of departure for an open-ended dialogue that is too elusive and alive to be limited by foundational constraints that are alien to the subject matter.