Fermat’s Last Theorem — how it works

So I spent two months trying to teach a proof of Fermat’s Last Theorem (FLT) on a computer. Much of the “how to” is a bit tedious and technical to explain: to cut a long story short, Wiles proved an “R = T” theorem and most of the work so far has been on computer instruction what are R and T; we haven’t finished any definition yet. However, my PhD student Andrew Yang has already proved the abstract commutative algebra result we need (“if the abstract rings R and T satisfy many technical conditions then they are equal”), and this is an exciting first step. The current writing status is HEREand the system we use is thin and its mathematical library mathlibmaintained by Lean prover community. If you know a little Lean and a little number theory then please read on contribution guidelinescheckout the project dashboard and claim a ISSUES. Like I said, we’re two months old. But we now have an interesting story, which I feel is worth sharing. Who knows if this is a sign of what’s to come.

We did not formalize the old 1990s proof of FLT. Since then, the work of many people (Diamond/Fujiwara, Kisin, Taylor, Scholze and others) has led to proofs that have been generalized and simplified, and part of the motivation for my work is not just getting FLT on line but to prove. these more general and powerful results. Why? Because if the AI ​​revolution in mathematics actually happens (which it will) and if Lean becomes an important component (which it will) then computers will be in a better position to start helping people to push the boundaries of modern number theory because of this formalization work, because they have access to key modern definitions in a form they can understand. A concept that was not used in the original proof of Wiles but used in the proof that we formalized, is crystalline cohomology, a theory developed in the 60s and 70s in Paris, whose foundations were laid by Berthelot following the ideas said Grothendieck. The basic idea here is that the classical exponential and logarithm functions play an important role in differential geometry (relating Lie algebras and Lie groups, for example), and especially in the understanding of de Rham cohomology, but it is not works in more arithmetic situations (e.g. behavior p); the theory of “divided power structures”, developed in the 1960s in a series of beautiful papers by Roby, played an important role in making an analogue of these functions applicable to the case of arithmetic. tl;dr: we need to teach computer crystalline cohomology, so we need to teach these divided powers first.

Antoine Chambert-Loir and Maria Ines de Frutos Fernandez taught the theory of divided powers to Lean, and over the summer Lean did that annoying thing it sometimes does: it complained about showing people a argument in the standard literature, and on closer inspection it turns out that the man’s argument leaves something to be desired. In particular a key lemma in Roby’s work seems incorrect. When Antoine told me this in a DM, he said he thought it was funny, and indeed the very long string of funny emojis he got back in response to his message proved it. However, Antoine, who is much more professional than me, argued that instead of me tweeting about the issue (which I couldn’t do because I left Twitter and joined blue sky yesterday), we really need to try to fix the problem. We do it differently. Antoine put it on his list of work to look at, and I completely ignored the problem and just started occasionally talking to people that the proof is in trouble, in a weak sense. I say “in a weak sense” because this observation needs to be put into some context. According to the way I now look at mathematics (as a formalist), the entire theory of crystalline cohomology disappeared from the literature the moment Antoine discovered the issue, with great collateral damage (i.e. large pieces of Scholze’s work just disappeared, entire books and papers vaporized etc.). But this loss is only temporarily. Crystal cohomology is in no practical sense “wrong”. The theorems are undoubtedly still TRUEit’s just that the proofs are as far as I know incomplete (or at least, the predecessors of Antoine and Maria Ines are), and unfortunately, it’s our job to fix it. The thing I want to emphasize is that it is absolutely clear to me and to Antoine that the proofs of the main results are of course. healalthough an intermediate lemma is wrong, because crystalline cohomology has been used so much since the 1970s that if there was a problem with it, it would have been known long ago. Every expert I spoke to was in complete agreement on this point (and several even said that I had no trouble about anything, but perhaps they did not understand what formalization really means in practice: you can’t just say “I’m sure it will be fixed” – you have to it will be fixed). An additional twist is that Roby, Grothendieck and Berthelot are all dead, so we can’t go back to the original experts and ask for help directly.

(For those interested in more technical details, here they are: Berthelot’s thesis did not develop the theory of divided powers from scratch, he used Roby’s “Les algebres a puissances dividees”, published in Bull Sci Math, 2ieme serie, 89, 1965, pages 75-91 Lemme 8 (on p86) in that paper seems false and it is not clear how to fix the proof; the proof of the lemma misquotes Roby’s other lemma from his 1963 Ann Sci ENS paper the correct statement is Gamma_A(M) tensor_A R = Gamma_R(M tensor_A R) but one of the tensor products is accidental falls in; The application breaks Roby’s proof that the divided power algebra of a module has a divided power, and thus prevents us from determining ring. A_{cris}.)

So as I said, Antoine worked on fixing the problem, while I just worked on gossiping about it with experts, and I made the mistake of telling Tadashi Tokieda about it in a coffeeshop in Islingtonhe went back to Stanford and mentioned it to Brian Conrad, and the next thing I knew Conrad was in my inbox asking me what this whole crystalline cohomology thing was wrong. I explained the technical details of the issue, Conrad agreed that there seemed to be a problem and he went to think about it. A few hours later he came back to me and pointed out that another, different, proof of the claim that the universal divided algebra of the power of a module has a divided power is in the appendix of the Berthelot-Ogus book on crystalline cohomology, and that so far as Conrad was concerned this method should be good. The proof is back!

And that’s the end of the story, except for the fact that last month I visited Berkeley and I had lunch with Arthur Ogus, who I’ve known since I was a post-doc there in the 90s. I promised Arthur a story about how he saved Fermat’s Last Theorem, and after dinner I told him how I dug his appendix out of a hole. His response was “Oh! That appendix has a lot of mistakes in it! But it’s OK, I think I know how to fix it.”

This story really highlights, to me, the poor job people do of documenting modern mathematics. It appears that there are many things that “experts know” but are not properly documented. Experts agree that important ideas are strong enough to withstand knocks like these, but the details what is actually happening may not be where you expect them to be. To me, this is just one of the many reasons why people want to consider math writing TRUEie in a formal system, where the chances of error are orders of magnitude smaller. However, most mathematicians are not formalists, and for people I have to justify my work in a different way. For mathematicians, I argue that teaching machines our arguments is an important step to getting machines to do it themselves. Until then, it seems we are destined to fix human errors by hand.

The story has a happy ending though – two weeks later it was given by Maria Ines a speech about the formalization of divided powers in the Cambridge Formalization of Mathematics seminar (started by Angeliki Koutsoukou-Argyraki a few years ago — thanks Angeliki!), and my understanding of Maria Ines’ talk is that these issues have been resolved already. So we are really back on track. Until the next time literature brings us down…