Why the proof of Fermat's Great Theorem does not need improvement

Over the decades since the landmark proof of Fermat’s great theorem, several ideas have emerged on how to make it even more reliable. However, these attempts reflect a deep misunderstanding of what makes evidence important.

June 23 marks the 25th anniversary of the announcement of Andrew Wiles , which excited everyone, in which he announced the proof of Fermat’s great theorem , the most famous problem in mathematics at the age of 350 years. The story surrounding Wiles' evidence - he worked secretly on this project for seven years, the evidence gap that emerged after the June announcement, an elegant solution published a year later in a joint work written by Wiles with his former student Richard Taylor , receiving a knighthood in 2000 - entered the annals of mathematical legends.



After Wiles' breakthrough, one can often hear speculations about the advent of a new “golden era” in mathematics, especially in number theory - the field to which Fermat's theorem belongs. The methods presented by Wiles and Taylor are today part of the toolkit of number theory experts who consider the history of the Great Theorem closed. But this story touched not only specialists in number theory.



I was suddenly reminded of this by the events of 2017, when, in the interval of several days, two logicians who made reports on two different continents pointed to ways to improve the proof of the Theorem - and told how surprised their colleagues were when experts in number theory did not show to their ideas are of no interest.

')

Logicians expressed these ideas in the languages ​​of their respective specialties - set theory and theoretical informatics. The proposals they made were inherently true, and perhaps someday they would raise new questions, no less interesting than those of Fermat. However, it immediately became clear to me that these questions are not related to specialists in number theory, and any other assumptions reflect a deep misunderstanding of the nature of Wiles' proof and the goals of number theory in general.



The roots of this misunderstanding can be found in the simplicity of the statement of the Theorem, which is responsible for most of its attractiveness: if n is any positive integer greater than 2, then it is impossible to find three such positive numbers, a, b and c, such that:

$$

$$a ^ n + b ^ n = c ^ n$$

This contrasts sharply with the case when n is 2: any person who has studied Euclidean geometry will remember that 3 ² + 4 ² = 5 ² , that 5 ² + 12 ² = 13 ² , and so on (this list is endless). Over the past few centuries, mathematicians have tried to explain the existence of such a contrast, and each time they have failed, however, leaving behind them whole new branches of mathematics. Among these branches are large areas of modern number theory, attracted by Wiles for his successful solution, as well as many fundamental ideas in every part of the science touched by mathematicians. And yet no one before Wiles could prove Fermat's claim.



Computer scientists have recently felt excited to learn about the progress made in automatically confirming evidence - an ambitious attempt to put the formalist approach to mathematics into practice. For formalists, mathematical proof is a list of statements that satisfy strict restrictions:

1. Statements at the top of the list should include generally accepted ideas. In a rigorous interpretation, this includes only the axioms of the formal set theory, usually from the formal system known as ZFC (Zermelo-Frenkel system with the axiom of choice). This is completely impractical, therefore we also allow the inclusion of already proved theorems - for example, the Great Theorem for the case n = 4, which Fermat himself proved in the 17th century.
2. Each subsequent statement must be obtained by applying the rules of logical deduction to the previous statements.
3. Finally, the proved theorem should be in last place on the list.

Mathematical logic was developed in the hope of establishing mathematics on a solid foundation - as an axiomatic system free of contradictions, which is able to reason without slipping into inconsistency. Although Kurt Gödel’s work showed that this dream was impossible, many philosophers from mathematics, as well as some logicians (a small but active minority, according to set theory experts), still refer to ZFC and the mentioned requirements as some kind of constitution from mathematics.



However, mathematicians never write evidence in this way. A logical analysis of Wiles' evidence points to many steps that do not take ZFC into account, with potential for scandal: if mathematicians come up with rules without checking for constitutionality, how do they know that they all mean the same thing?



Automatic evidence verification seems to offer a solution to this problem. It involves reformulating the evidence through a set of separate statements, each of which is written in a consistent language that the computer can read, and then confirm the constitutional fidelity of each step. This time-consuming method has been successfully applied to many long and complex proofs, the most famous of which is the proof of Kepler's hypothesis on the densest packing of spheres made by Thomas Hales. Testing Wiles' evidence has long been considered one of the main goals. Therefore, my friend, an expert in computer science, was genuinely disappointed that the search for "pure mathematicians who categorically support the use of automatic tools in constructing their arguments", as he formulated, has not yet yielded results.





" Arithmetic " of Diophantus edition of 1670, in which Fermat’s notorious note is included in the main text. It is translated as follows: “It is impossible for a cube to be the sum of two cubes, for the fourth degree it is impossible to be the sum of two fourth degrees, or, in general, for any number representing a degree greater than the second, it is impossible to be the sum of two of the same degrees. I have discovered truly wonderful evidence of this assumption, for which these fields are too narrow to place here. "



The first thing that does not take into account this disappointment is that Wiles' evidence, albeit complex, has a simple basis that is easy to explain to a narrow-minded audience. Suppose that, contrary to Fermat’s statement, there are three positive integers a, b, c such that



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



for some odd prime p (and it’s enough to consider only prime numbers). In 1985, Gerhard Frey showed that a, b, and c can be rearranged into



(B) a new equation called "elliptic curve"



with properties that everyone thought were impossible. More precisely, it has long been known how to express this elliptic curve in terms of



(C) Galois representation



which is an infinite set of equations related both to the elliptic curve and to each other by clear rules.



The connection between these steps was well known in 1985. By that time, most experts in number theory were convinced - although there was no evidence so far - that each Galois representation could be assigned, again, according to clear rules,



(D) a modular function,



something like a two-dimensional generalization of familiar sine and cosine functions from trigonometry.



The final link was obtained when Ken Ribet confirmed the assumption of Jean-Pierre Seur that the properties of a modular function given by the form of the Frey elliptic curve imply the existence



(E) another modular function of weight 2 and level 2.



However, such functions cannot exist. Therefore, there exists neither a modular function (D), nor a Galois representation (C), nor equation (B), nor a solution (A).



It only remained to find the missing link between (C) and (D), which mathematicians called the modularity hypothesis.



This link has been the subject of a seven-year search for Wiles. From our current point of view, it is difficult to fully appreciate the courage of this risky enterprise. Twenty years after Yutaka Taniyama and Goro Shimura first reported the relationship between (B) and (D) through (C) in the 1950s, mathematicians gradually came to the conclusion that this should be so. This hope was expressed in a very popular work by Andre Weil, which fit perfectly into the extremely influential Langlands program , named after the Canadian mathematician Robert Langlands. This connection was too good not to be true. However, the modularity hypothesis seemed completely unattainable. Objects of types (C) and (D) were too different.



The computer scientist didn’t explain whether his disappointment was due to the fact that it wasn’t important for number theory that the proof was limited to finding the critical link between (C) and (D), or that it ranged from (A) to (E). I will not try to figure it out. But if the logicians only needed to formally confirm the published proof of the connection between (C) and (D), then their expectations were too high. First, Wiles proved only a little more than enough for the modularity hypothesis to complete the deduction “from (A) to (E)”. The complete hypothesis of modularity was established several years later by Christoph Broglie, Brian Conrad, Fred Diamond and Richard Taylor. But this does not cast a shadow on Wiles's work! On the contrary, the fact that such a large number of the world's leading experts in number theory followed in the footsteps of Wiles' work just a few months after its appearance speaks of its wealth.



For example, a little later, in the fall of 2016, 10 mathematicians met at the Advanced Research Institute in Princeton, New Jersey, and were able to prove the connection between elliptic curves and modular functions under new conditions. They all used different paths to understand the structure of Wiles' evidence, which appeared when some of them were still children. If they were asked to describe this proof in the form of a sequence of logical conclusions, they would undoubtedly have issued 10 different versions of it. Each of them would resemble the path from (A) to (E) described above, but would be much more detailed.



Nevertheless - and this is always overlooked from the philosophical view of evidence - each of these ten would attribute authorship of its evidence to Wiles. They would refer to them in the same way as other evidence studied by them in explanatory articles or in the training courses they attended or taught. And although each of the ten would have omitted some details, in general they would all be right.



What is Wiles evidence if it can have so many different options? In mathematical philosophy, it is customary to treat a published proof as an approximation to an ideal formalized proof, which in principle can be checked on a computer that applies the rules of a formal system. Ideal evidence is not contaminated by anything outside the formal system - as if every law bore a mark confirming its constitutional justification.



But this approach contradicts what mathematicians themselves say about their evidence. Mathematicians do not use ideological or philosophical litmus tests, but I am convinced that most of my colleagues will agree with Michael Francis Atiyah, who stated that the proof “is the final test, but not the basis of anything.” The published evidence is clearly not the foundation of anything.



Wiles and specialists in number theory, refining and expanding his ideas, certainly did not expect to receive offers from two logicians. But - unlike many people observing number theory from afar - they definitely understood that such proof as the one published by Wiles should not be treated as a kind of artifact in itself. On the contrary, Wiles' proof is the starting point of an open dialogue that is too elusive and lively to be limited to serious limits that are alien to the subject.