https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/ Xena Mathematicians learning Lean by doing. [cropped-light2] Skip to content * Home * About Xena * Student projects * What maths is in Lean? * Installing Lean and mathlib * Twitter * Useful links. - Lean in 2024 Fermat's Last Theorem -- how it's going Posted on December 11, 2024 by xenaproject So I'm two months into trying to teach a proof of Fermat's Last Theorem (FLT) to a computer. Most of "how it's going" is quite tedious and technical to explain: to cut a long story short, Wiles proved an "R=T" theorem and much of the work so far has gone into teaching the computer what R and T are; we still have not finished either definition. However my PhD student Andrew Yang has already proved the abstract commutative algebra result which we need ("if abstract rings R and T satisfy lots of technical conditions then they're equal"), and this is an exciting first step. The current state of the write-up is here, and the system we are using is Lean and its mathematical library mathlib, maintained by the Lean prover community. If you know a bit of Lean and a bit of number theory then feel free to read the contribution guidelines, checkout the project dashboard and claim an issue. As I say, we're two months in. However we already have one interesting story, which I felt was worth sharing. Who knows if it's an indication of what is to come. We're not formalising the old-fashioned 1990s proof of FLT. Since then, work of many people (Diamond/Fujiwara, Kisin, Taylor, Scholze and several others) led to the proof being generalised and simplified, and part of the motivation of my work is not to just get FLT over the line but to prove these more general and powerful results. Why? Because if the AI mathematics revolution actually happens (which it might) and if Lean turns out to be an important component (which it might) then computers will be in a better position to start helping humans to push back the boundaries of modern number theory because of this formalization work, as they'll have access to key modern definitions in a form which they understand. One concept which was not used in Wiles' original proof but which is being used in the proof we're formalizing, is crystalline cohomology, a theory developed in the 60s and 70s in Paris, with the foundations laid down by Berthelot following ideas of Grothendieck. The basic idea here is that the classical exponential and logarithm functions play a key role in differential geometry (relating Lie algebras and Lie groups, for example), and in particular in understanding de Rham cohomology, but they do not work in more arithmetic situations (for example in characteristic p); the theory of "divided power structures", developed in the 1960s in a series of beautiful papers by Roby, play a crucial role in constructing an analogue of these functions which can be used in the arithmetic case. tl;dr: we need to teach the computer crystalline cohomology, so first we need to teach it divided powers. Antoine Chambert-Loir and Maria Ines de Frutos Fernandez have been teaching the theory of divided powers to Lean, and over the summer Lean did that irritating thing which it sometimes does: it complained about the human presentation of an argument in the standard literature, and on closer inspection it turned out that the human argument left something to be desired. In particular a key lemma in Roby's work seems to be incorrect. When Antoine told me this in a DM, he remarked that he would suppose I thought this was funny, and indeed the very long string of laughing emojis which he got back as a response to his message confirmed this. However Antoine, being rather more professional than me, argued that instead of me tweeting about the issue (which I can't do anyway because I left Twitter and joined bluesky yesterday), we should in fact attempt to fix the problem. We went about this in rather different ways. Antoine put it on his job list to look at, and I completely ignored the problem and just started occasionally mentioning to people that the proof was in trouble, in a weak sense. I say "in a weak sense" because this observation has to be put into some context. According to the way I currently view mathematics (as a formalist), the entire theory of crystalline cohomology vanished from the literature at the moment Antoine discovered the issue, with massive collateral damage (for example huge chunks of Scholze's work just disappeared, entire books and papers vaporised etc). But this disappearance is only temporary. Crystalline cohomology is in no practical sense "wrong". The theorems were still undoubtedly correct, it's just that the proofs were as far as I am concerned incomplete (or at least, the ones Antoine and Maria Ines were following were), and unfortunately it is now our job to fix them. The thing I want to stress is that it was absolutely clear to both me and Antoine that the proofs of the main results were of course going to be fixable, even if an intermediate lemma was false, because crystalline cohomology has been used so much since the 1970s that if there were a problem with it, it would have come to light a long time ago. Every expert I've spoken to is in complete agreement on this point (and several even went so far as to claim that I'm making a fuss about nothing, but perhaps they don't understand what formalization actually means in practice: you can't just say "I'm sure it's fixable" -- you have to actually fix it). One added twist is that Roby, Grothendieck and Berthelot have all died, so we could not go back to the original experts and ask directly for help. [For those that are interested in more technical details, here they are: Berthelot's thesis does not develop the theory of divided powers from scratch, he uses Roby's "Les algebres a puissances divisees", published in Bull Sci Math, 2ieme serie, 89, 1965, pages 75-91. Lemme 8 (on p86) of that paper seems to be false and it's not obvious how to repair the proof; the proof of the lemma misquotes another lemma of Roby 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 accidentally falls off in the application. This breaks Roby's proof that the divided power algebra of a module has divided powers, and thus stops us from defining the ring A_{cris}.] So as I say, Antoine worked on fixing the problem, whereas I just worked on gossiping about it to the experts, and I made the mistake of telling Tadashi Tokieda about it in a coffeeshop in Islington, he duly went back to Stanford and mentioned it to Brian Conrad, and the next thing I knew Conrad was in my inbox asking me what was all this about crystalline cohomology being wrong. I explained the technical details of the issue, Conrad agreed that there seemed to be a problem and he went off to think about it. Several hours later he got back to me and pointed out that another, different, proof of the claim that the universal divided power algebra of a module had divided powers was in the appendix to the Berthelot-Ogus book on crystalline cohomology, and that as far as Conrad was concerned this approach should be fine. The proof was back on! And that is pretty much the end of the story, other than 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'd promised Arthur a story of how he'd saved Fermat's Last Theorem, and over the meal I told him about how his appendix had dug me out of a hole. His response was "Oh! That appendix has several errors in it! But it's OK, I think I know how to fix them." This story really highlights, to me, the poor job which humans do of documenting modern mathematics. There appear to be so many things which are "known to the experts" but not correctly documented. The experts are in agreement that the important ideas are robust enough to withstand knocks like this, but the details of what is actually going on might not actually be where you expect them to be. For me, this is just one of many reasons why humans might want to consider getting mathematics written down properly, i.e. in a formal system, where the chances of error are orders of magnitude smaller. However most mathematicians are not formalists, and for those people I need to justify my work in a different way. For those mathematicians, I argue that teaching machines our arguments is a crucial step towards getting machines to do it themselves. Until then, we seemed to be doomed to fix up human errors manually. The story does have a happy ending though -- two weeks ago Maria Ines gave a talk about formalization of divided powers in the Cambridge Formalization of Mathematics seminar (which was started by Angeliki Koutsoukou-Argyraki a couple of years ago -- thanks Angeliki!), and my understanding of Maria Ines' talk is that these issues have now been sorted out. So we are actually back on track. Until the next time the literature lets us down... Share this: * Twitter * Facebook * Like Loading... Related [e7ccfd4] About xenaproject The Xena Project aims to get mathematics undergraduates (at Imperial College and beyond) trained in the art of formalising mathematics on a computer. Why? Because I have this feeling that digitising mathematics will be really important one day. View all posts by xenaproject - This entry was posted in Fermat's Last Theorem, Research formalisation and tagged crystalline cohomology, Fermat's Last Theorem, lean, logic, math, mathematics, maths, Peter Scholze, philosophy. Bookmark the permalink. - Lean in 2024 15 Responses to Fermat's Last Theorem -- how it's going 1. [a5ca] David Loeffler says: December 12, 2024 at 10:13 am Hi Kevin, Just to play devil's advocate a bit: you write The thing I want to stress is that it was absolutely clear to both me and Antoine that the proofs of the main results were of course going to be fixable, even if an intermediate lemma was false, because crystalline cohomology has been used so much since the 1970s that if there were a problem with it, it would have come to light a long time ago. Why does the fact that people have used crystalline cohomology successfully constitute evidence that its foundational lemmas are provable? There are a fair number of papers in analytic number theory that assume the Riemann hypothesis; none of these have run into any obvious contradictions, and that might be some (weak) evidence for believing that RH is true, but doesn't in any way imply that a proof of it is on the cards any time soon. Certainly if numerous people had actually sceptically examined the foundations of crystalline cohomology, then that would be good evidence it is correct; but evidently they haven't, or the mistake in Roby's work would already have been identified and fixed - rather, people are using crystalline cohomology as a black box and building new stuff on top of it, not looking inside the box. Of course, this ultimately only strengthens the case for a large-scale formalisation of the literature. LikeLiked by 1 person Reply + [e7cc] xenaproject says: December 12, 2024 at 11:40 am Hi David! So I told a few experts this story (at various points during its evolution), and basically got two very distinct responses. There was the "yes this sort of story clearly indicates that what you're doing is a great thing" response, and there was the "well obviously there are loads of different ways of doing crystalline cohomology these days, I mean you can do it the prismatic way, clearly something works, the experts have checked everything, this is not a story" response. I guess what separates these two positions is how much value you assign to the existence of some canonical reference which everyone is 100% confident is watertight, as opposed to just knowing what must be true (and being confident that the current tools available to humanity would be enough to check it and even that "it's probably in the literature somewhere") and not worrying too much about why. LikeLike Reply o [a5ca] David Loeffler says: December 12, 2024 at 12:06 pm ...just knowing what must be true (and being confident that the current tools available to humanity would be enough to check it) What if this confidence is misplaced? This is precisely my nightmare scenario: that "everyone" - i.e. the small community of experts in some given area - might be, collectively, wrong in their estimation about what is readily provable with available tools. LikeLike + [7c9f] Ahmad AK says: December 12, 2024 at 3:46 pm Could it be argued that in algebraic number theory, abstract results have much more immediate "concrete" consequences than in analytic number theory so that contradictions have a higher chance of manifesting themselves? Analytic number theory results tend to deal with the very large or have a probabilistic nature two aspects which make translating into concrete results difficult, and hence contradictions can remain hidden for a long time, for example what would a potential contradiction to szemeredi regularity lemma or the Green-Tao Theorem look like? LikeLike Reply + [95fa] melbur says: December 12, 2024 at 5:50 pm Using crystalline cohomology successfully suggests its foundational lemmas are likely correct because consistent, accurate results imply robustness. However, this is indirect evidence, not a guarantee of provability. It's like assuming the Riemann hypothesis is true because it hasn't led to contradictions in its applications--suggestive but not definitive proof. A large-scale formal review of crystalline cohomology's foundations would strengthen confidence, especially by addressing any overlooked issues, as mistakes can persist unnoticed when concepts are used as "black boxes" rather than critically examined. LikeLike Reply 2. [2cf3] andy says: December 12, 2024 at 3:21 pm Just out of curiosity, was there a reason that stacks project was not the first option at finding a human reference proof? I would think the ability for people to comment and point out errors would probably make it have less mistakes than math texts in general-of course I'm in full agreement that much of existing literature of math in general have too many fixable small errors. LikeLike Reply + [e7cc] xenaproject says: December 13, 2024 at 12:27 pm This is a good question (I've also been asked it in person by Toby Gee and on Bluesky by Daniel Litt). What we actually need is the ring B_{cris}. Does Stacks do enough to make this ring? I don't recall seeing divided power envelopes done in the generality needed for the definition of B_{cris} there (don't they just do divided power algebras in one variable or something?). Antoine's instinct was to go to the source. Note that we have already established that there *is* a (mostly) correct proof in the literature (in the appendix to Berthelot-Ogus). LikeLike Reply 3. [6ac6] Darij Grinberg says: December 12, 2024 at 7:23 pm Divided power algebras of non-free modules are a notorious minefield. I am highly grateful to Lundkvist for his paper https: //doi.org/10.1016/j.jpaa.2008.03.024 that has saved me a lot of time I would have wasted proving things that are not true. But this is a new one to me, as I have never read Norbert Roby's work (it's in French) nor anything about crystalline cohomology. Instead, I know divided power algebras mainly through the work of Rota & co (including an appendix in Eisenbud's "With a View"), who take care to only apply the construction to free modules, and through the Stacks Project, which does many interesting things with DPAs ( https://stacks.math.columbia.edu/download/dpa.pdf ) but never claims anything this strong. So it's not all literature, just the algebraic geometry/number theory one perhaps Now you've made me curious: What is the status of Roby's claim? Is there a counterexample or just a gap in the proof? LikeLike Reply 4. [6ac6] Darij Grinberg says: December 12, 2024 at 7:42 pm Incidentally, I cannot find the Roby paper you are citing. The volume does not correspond the year on http://www.numdam.org/item /BSMF/ . Is this a case of two journals sharing an abbreviation? LikeLike Reply + [e7cc] xenaproject says: December 13, 2024 at 12:11 pm Yes it looks like it is -- Roby's paper is https://zbmath.org/ 0145.04503 LikeLike Reply o [6ac6] Darij Grinberg says: December 13, 2024 at 1:15 pm Interesting. It's not available online anywhere? LikeLike 5. [ce9c] pvessenes says: December 12, 2024 at 8:59 pm I'm way, way down the chain from serious mathematicians, but I did get a math degree in the 1990s. David, I think the intuition here is that to the extent crystalline cohomology gives results that are falsifiable, and not existing in some weird either-or axiom-of-choice type universe where you can get internally consistent mathematics positing either side, then there have been many strong results coming from it and those all.. hold together. The idea that you'd have a branch of mathematics that would be not just built on shaky foundations, but would be totally incorrect, but still give consistently correct and useful results I think is one that's a little far-fetched to mathematicians. Like, we would say today that Calculus / Real Analysis wasn't really formalized until Weierstrass and Dedekind in the late 1800s. But, you know, Newton would have told you he didn't care about your this-ing and that-ing about the reals and fancy complaints about how limits work -- the Calculus was absolutely correct. And he would have been right. And to be clear, Newton's calculus was in particular very hand-wavy compared to the post-Liebniz formalization we build on today. I think none of this bothers working mathematicians -- the entire edifice of modern mathematics has been built on this sort of iterative refinement of true but possibly incorrectly formulated or proven truth, for thousands of years, and it's only recently in the last few decades that the hundred-year-old formalization movement seems to have gotten enough legs with theorem provers to really look seriously at completing the project. LikeLike Reply + [a5ca] David Loeffler says: December 13, 2024 at 3:47 pm The idea that you'd have a branch of mathematics that would be not just built on shaky foundations, but would be totally incorrect, but still give consistently correct and useful results I think is one that's a little far-fetched to mathematicians. Well, I'm a mathematician myself and I don't find it far-fetched! I don't know of any actual examples where this has happened, but there have been some worryingly close near-misses. LikeLike Reply o [a5ca] David Loeffler says: December 13, 2024 at 4:27 pm PS: Of course, this depends a lot on what you mean by "totally incorrect". If "incorrect" for you means "leads to contradictions", then your statement is true, but arguably vacuously so. On the other hand, if "incorrect" means "apparently consistent but has not been proved", then I think this very much could happen. But perhaps this is what you meant by "built on shaky foundations"; so I'm not longer sure I know what your post means - what scenario do you have in mind? LikeLike 6. [d9c4] Srivatsa Srinivas says: December 13, 2024 at 3:50 pm "Because if the AI mathematics revolution actually happens (which it might) and if Lean turns out to be an important component (which it might) then computers will be in a better position to start helping humans to push back the boundaries of modern number theory because of this formalization work, as they'll have access to key modern definitions in a form which they understand." If AI can actually write non trivial proofs there would be no point in formalizing as the AI would probably either rediscover everything itself AlphaZero style or just be good enough to translate PDFs into Lean code automatically. Luckily, I do believe that AI won't reach that point anytime soon, so formalizing is a worthy goal LikeLike Reply Leave a comment Cancel reply [ ] [ ] [ ] [ ] [ ] [ ] [ ] D[ ] * Search for: [ ] [Search] * Categories + Algebraic Geometry + computability + Fermat's Last Theorem + formalising mathematics course + General + Imperial + Learning Lean + liquid tensor experiment + M1F + M1P1 + M40001 + M4P33 + Machine Learning + number theory + Olympiad stuff + Research formalisation + rigour + tactics + Technical assistance + Type theory + Uncategorized + undergrad maths * Recent Posts + Fermat's Last Theorem -- how it's going December 11, 2024 + Lean in 2024 January 20, 2024 + Formalising modern research mathematics in real time November 4, 2023 + Lean 2022 round-up January 8, 2023 + Beyond the Liquid Tensor Experiment September 12, 2022 Xena Blog at WordPress.com. [Close and accept] Privacy & Cookies: This site uses cookies. By continuing to use this website, you agree to their use. To find out more, including how to control cookies, see here: Cookie Policy * Comment * Reblog * Subscribe Subscribed + [croppe] Xena Join 179 other subscribers [ ] Sign me up + Already have a WordPress.com account? Log in now. * + [croppe] Xena + Customize + Subscribe Subscribed + Sign up + Log in + Copy shortlink + Report this content + View post in Reader + Manage subscriptions + Collapse this bar %d [b] Design a site like this with WordPress.com Get started