Fermat's Last Theorem – how it’s going

This reminds me of a fun experience I had in grad school. I was working on writing some fast code to compute something I can no longer explain, to help my advisor in his computational approach to the Birch and Swinnerton-Dyer conjecture. I gave a talk at a number theory seminar a few towns over, and was asked if I was doing this in hopes of reinforcing the evidence behind the conjecture. I said with a grin, &quot;well, no, I&#x27;d much rather find a counterexample.&quot; The crowd went <i>wild</i>; I&#x27;ve never made a group of experts so angry as that day.<p>Well, I never was much of a number theorist. I never did come to understand the basic definitions behind the BSD conjecture. Number theory is so old, so deep, that writing a PhD on the topic is the step one takes to become a novice. Where I say that I didn&#x27;t understand the definitions, I certainly knew them and understood the notation. But there&#x27;s a depth of intuition that I never arrived at. So the uproar of experts, angry that I had the audacity to hope for a counterexample, left me more curious than shaken: what do they see, that they cannot yet put words to?<p>I am delighted by these advances in formalism. It makes the field feel infinitely more approachable, as I was a programmer long before I called myself a mathematician, and programming is still my &quot;native tongue.&quot; To the engineers despairing at this story, take it from me: this article shows that our anxiety at the perceived lack of formalism is justified, but we must remember that anxiety is a feeling -- and the proper response to that feeling is curiosity, not avoidance.

I remember when I was a student a friend of mine telling me this guy was giving a seminar and he&#x27;d just completed day one and everyone was really excited he was going to prove FLT. Of course, the guy in question was Andrew Wiles. He then spent months patching up problems they found prior to publication and finally the whole thing got published. It was a hugely exciting thing when you were studying mathematics.<p>All of which is a long way of saying the line &quot;the old-fashioned 1990s proof&quot; makes me feel _really_ old.

&gt; 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.<p>Tongue-in-cheek irritation aside, this is actually awesome. I think Lean (and other theorem provers) are going to end up being important tools in math going forward.

&gt; 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.<p>It makes me think about how you get UI&#x2F;UX&#x2F;web designers who make (informal, imprecise) mockups and prototypes of their design ideas and interaction flows, they then hand these off to a developer to do the coding (formalise it, explain it precisely to the machine), and on the way the developer will inevitably find problems&#x2F;holes in the designs (like an interaction scenario or code path not considered in the design, which could uncover a major design flaw), which the developer and&#x2F;or the designer will have to patch somehow.<p>As in, design and development are different roles and require different mindsets, and most designers have a very strong resistance against working and thinking like a developer.

If you&#x27;re interested in this stuff at all, check out some code.<p>Example: <a href="https:&#x2F;&#x2F;github.com&#x2F;ImperialCollegeLondon&#x2F;FLT&#x2F;blob&#x2F;main&#x2F;FLT&#x2F;Mathlib&#x2F;Algebra&#x2F;GroupWithZero&#x2F;NonZeroDivisors.lean" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;ImperialCollegeLondon&#x2F;FLT&#x2F;blob&#x2F;main&#x2F;FLT&#x2F;M...</a><p>Also check out the blueprint, which describes the overall structure of the code:<p><a href="https:&#x2F;&#x2F;imperialcollegelondon.github.io&#x2F;FLT&#x2F;blueprint&#x2F;" rel="nofollow">https:&#x2F;&#x2F;imperialcollegelondon.github.io&#x2F;FLT&#x2F;blueprint&#x2F;</a><p>I&#x27;m very much an outside observer, but it is super interesting to see what Lean code looks like and how people contribute to it. Great thing is that there&#x27;s no need for unittests (or, in some sense, the final proof statement <i>is</i> the unittest) :P

&gt; 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.<p>Past researcher in pure math here. The big problem is that mathematicians are notorious for not providing self-contained proofs of anything because there is no incentive to do so and authors sometimes even seem proud to &quot;skip the details&quot;. What actually ends up happening is that if you want a rigorous proof that can be followed theoretically by every logical step, you actually need an expert to fill in a bunch of gaps that simply can&#x27;t easily be found in the literature. It&#x27;s only when such a person writes a book explaining everything that it might be possible, and sometimes not even then.<p>The truth is, a lot of modern math is on shaky ground when it comes to stuff written down.

&gt; 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.<p>I&#x27;ve always wondered if this intuition was really true. Would it really be so impossible for a whole branch of mathematics to be developed based on a flawed proof and turn out to be simply false?

For the past year or so, I&#x27;ve been trying (off and on) to formalise part of my undergraduate complex analysis course in Lean. It has been instructional and rewarding, but also sometimes frustrating. I only recently was able to fully define polar form as a bijection from C* to (-pi,pi] x R, but that&#x27;s because I insisted on defining the complex numbers, (power) series, exp and sin &quot;from scratch&quot;, even though they&#x27;re of course already in mathlib.<p>Many of my troubles probably come from the fact that I only have a BSc in maths and that I&#x27;m not very familiar with Lean&#x2F;mathlib and don&#x27;t have anyone guiding me (although I did ask some questions in the very helpful Zulip community). Many results in mathlib are stated in rather abstract ways and it can be hard to figure out how they relate to certain standard undergraduate theorems - or whether those are in mathlib at all. This certainly makes sense for the research maths community, but it was definitely a stumbling block for me (and probably would be one if Lean were used more in teaching - but this is something that could be sorted out given more time).<p>In terms of proof automation, I believe we&#x27;re not there yet. There are too many things that are absolutely harder to prove than they should be (although I&#x27;m sure that there&#x27;s also a lot of tricks that I&#x27;m just not aware of). My biggest gripe concerns casts, in &quot;regular&quot; mathematics, the real numbers are a subset of the complex numbers and so things that are true for all complex numbers are automatically true for all reals[0], but in Lean they&#x27;re different types with an injective map &#x2F; cast operation and there is a lot of back-and-forth conversion that has to be done and muddies the essence of the proof, especially when you have &quot;stacks&quot; of casts, e.g. a natural number cast to a real cast to a complex number etc.<p>Of course, this is somewhat specific to the subject, I imagine that in other areas, e.g. algebra, dealing with explicit maps is much more natural.<p>[0] This is technically only true for sentences without existential quantifiers.

This thread seems to be about good writing for math.<p>Okay, for some decades, I&#x27;ve read, written, taught, applied, and published, in total, quite a lot of math. Got a Ph.D. in applied math.<p>Yes, there are problems in writing math, that is, some math is poorly written.<p>But, some math is quite nicely written. (1) Of course, at least define every symbol before using it. (2) It helps to motivate some math before presenting it. (3) Sometimes intuitive statments can help.<p>For more, carefully reading some well-written math can help learning how to write math well:<p>Paul R.\ Halmos, {\it Finite-Dimensional Vector Spaces, Second Edition,\&#x2F;} D.\ Van Nostrand Company, Inc., Princeton, New Jersey, 1958.\ \<p>R.\ Creighton Buck, {\it Advanced Calculus,\&#x2F;} McGraw-Hill, New York, 1956.\ \<p>Tom M.\ Apostol, {\it Mathematical Analysis: Second Edition,\&#x2F;} ISBN 0-201-00288-4, Addison-Wesley, Reading, Massachusetts, 1974.\ \<p>H.\ L.\ Royden, {\it Real Analysis: Second Edition,\&#x2F;} Macmillan, New York, 1971.\ \<p>Walter Rudin, {\it Real and Complex Analysis,\&#x2F;} ISBN 07-054232-5, McGraw-Hill, New York, 1966.\ \<p>Leo Breiman, {\it Probability,\&#x2F;} ISBN 0-89871-296-3, SIAM, Philadelphia, 1992.\ \<p>Jacques Neveu, {\it Mathematical Foundations of the Calculus of Probability,\&#x2F;} Holden-Day, San Francisco, 1965.\ \

Haha, that author is a funny writer. Very weird experience for that to be so readable, when I didn&#x27;t understand probably half the content.<p>By the way, I found an excellent word for when a proof is disproven or found to be faulty, but that is esoteric enough that it has less risk of being misinterpreted to mean the conclusion is proven false: &#x27;vitiated&#x27;. The conclusion might still be true, it just needs a new or repaired proof; the initial proof is &#x27;vitiated&#x27;. I like how the word sounds, too.

This article makes me very happy.<p>One of the many reasons I love math is the feeling I&#x27;ve always had that with it, we&#x27;re building skyscraper-sized mental structures that are built on provably indestructible foundations.<p>With the advent of &quot;modern&quot; proofs, which involve large teams of Mathematicians who produce proof that are multiple hundreds of pages long and only understandable by a very, very tiny sliver of humanity (with the extreme case of Shinichi Mochizuki [1] where N=1), I honestly felt that math had lost its way.<p>Examples: graph coloring theorem, Fermat&#x27;s last theorem, finite group classification theorem ... all of them with gigantic proofs, out of reach of most casual observers.<p>And lo and behold, someone found shaky stuff in a long proof, what a surprise.<p>But it looks like some Mathematicians feel the same way I do and have decided to do something about it by relying on the computers. Way to go guys !<p>[1] <a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Shinichi_Mochizuki" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Shinichi_Mochizuki</a>

This hurts my engineer-brain. Just a reminder than the gap between us and mathematicians is about the same as the gap between us and everybody else (edit: in terms of math skills), just in the other direction, haha.<p>Oh well, hopefully when they get the machines to solve math, they’ll still want them to run a couple percents faster every year.

I am extremely disappointed at the replies from (some) experts. As a mathematician who has been worrying about the state of the literature for some time, I expected trouble like this---and expect considerably more, especially from the number theory literature between the 60s and the 90s. I also wonder how well 4-manifold theory is faring.<p>Much worse, this nonchalant attitude is being taught to PhD students and postdocs both explicitly and implicitly: if you are worried too much, maybe you are not smart enough to understand the arguments&#x2F;your mathematical sense is not good enough to perceive the essence of the work. If you explain too much, your readers will think you think they are dumb; erase this page from your paper (actual referee feedback).<p>Also, like Loeffler in the comments, I don&#x27;t trust the &quot;people have been using crystalline cohomology forever without trouble&quot; argument. The basics are correct, yes, as far as I can tell (because I verified them myself, bearing in mind of course that I am very fallible).<p>But precisely because of that, large swathes of the theory <i>will</i> be correct. Errors <i>will</i> be rare and circumstantial, and that is part of the problem! It makes them very easy to creep into a line of work and go unnoticed for a long time, especially if the expert community of the area is tiny---as is the case in most sub-areas of research math.

This is the the talk by Dr de Frutos—Fernandez that Dr Buzzard mentions at the end: <a href="https:&#x2F;&#x2F;m.youtube.com&#x2F;watch?v=QCRLwC5JQw0" rel="nofollow">https:&#x2F;&#x2F;m.youtube.com&#x2F;watch?v=QCRLwC5JQw0</a>

Richard Feynman, while still a student at Princeton, found an error in some well known proof, and set himself a rule to double check every theorem he would use.<p>I don&#x27;t remember the details of the story (I read surely your joking years ago), and remember being amazed by how much time that policy must have cost him.<p>But now I wonder that he didn&#x27;t hit dozens or hundreds of errors over the years.

This makes me wonder if there&#x27;ll ever be a significant bug discovered in Lean itself, breaking past formalisation work.

One of my favorite Horizon episodes is the FLT one that features Prof. Andrew Wiles&#x27; development of his proof (I have watched it many times). Of course, it is grounded in Fermat&#x27;s margin note about his having a wonderful proof that couldn&#x27;t fit in said margin. At the end of the documentary, the various mathematicians in it note that AW&#x27;s proof certaintly wasn&#x27;t what PdF had in mind because AW&#x27;s proof is thorougly modern.<p>So I have wondered about PdF&#x27;s possible thinking.<p>Now, the degenerate case of n=2 is just the Pythagorean Theorem<p><pre><code> c^2 = a^2 + b^2 </code></pre> and we now know from AW&#x27;s proof that the cubic and beyond fail.<p>Now, the PT is successful because the square b^2 can be &quot;squished&quot; over the corner of a^2, leaving a perfect square c^2. [Let&#x27;s let the a^n part be the bigger of the two.]<p><pre><code> 5^2 = 4^2 + 3^2 25 = 16 + 9 25 = 16 + (4 + 4 + 1) </code></pre> Each of the 4&#x27;s go on the sides, and the 1 goes on the corner, leaving a pure 5x5 square left over.<p>Now, for cubes, we now know that a cube cannot be &quot;squished&quot; onto another cube&#x27;s corner in such a way that makes a bigger cube.<p>I&#x27;m not up for breaking out my (diminishing) algebra right now (as it&#x27;s a brain off day), but that b^3 cube would need to break down into three flat sides, three linear edges, and the corner.<p>This fits my physical intuition of the problem and seems to me to be a possible way that PdF might have visualized the cubic form. Now, I have zero mathematical intuition about such things (or necessary math skills either), but the physical nature of the problem, plus the fact that we now know that the cubic and beyond don&#x27;t work, leads me to wonder if this is an interesting approach. It also makes me curious to know why it isn&#x27;t, if that is indeed the case, (which I assume is probable).<p>As to the n=4 and beyond, I would just hand-wave them away and say something like, &quot;Well, of course they are more fractally impossible&quot;, which by that I mean that a real mathematician would have to say exactly why the n=3 case failing means that the n&gt;=4 case would also not work. (My guess here is that there just becomes less and less possibility of matching up higher-dimensional versions of a two-term addition.)<p>Anyway, just a thought I had some years ago. I even built a lego model of the bits of cube spreading out along the corner of the a^3 cube.<p>I would enjoy learning why I&#x27;m so utterly wrong about this, but I found it a fun mental exercise some years ago that&#x27;s been swimming around in my brain.<p>Thanks in advance if there are any takers around here. :-)<p>[And, my favorite Horizon episode is &#x27;Freak Wave&#x27;.]

Formalization of maths seems like an overwhelmingly huge task. A bit like Cyc but harder. Is there some kind of chain reaction likely to happen once a critical mass of math has been formalized so that it becomes easier to do more?

What is the simplest proof of FLT these days? I don’t think elementary proofs exist

Nice story, and I&#x27;m glad formalization work is proceeding. &quot;Details left as an exercise to the reader&quot; is the bane of true knowledge.

When this topic comes up I love sharing this talk by Sussman; because every time I watch it again!<p><a href="https:&#x2F;&#x2F;www.infoq.com&#x2F;presentations&#x2F;Expression-of-Ideas&#x2F;" rel="nofollow">https:&#x2F;&#x2F;www.infoq.com&#x2F;presentations&#x2F;Expression-of-Ideas&#x2F;</a>

Someone had to post this video of a song about Fermat - even if it’s in Dutch - legend: <a href="https:&#x2F;&#x2F;youtu.be&#x2F;X2AVi6RCgN8?si=ZnN9lMb-XuirZ20_" rel="nofollow">https:&#x2F;&#x2F;youtu.be&#x2F;X2AVi6RCgN8?si=ZnN9lMb-XuirZ20_</a>

I’m happy to see so much work going into fixing human errors in mathematics in a rigorous way.

<a href="https:&#x2F;&#x2F;www.techrxiv.org&#x2F;users&#x2F;717330&#x2F;articles&#x2F;702287-on-fermat-s-last-theorem" rel="nofollow">https:&#x2F;&#x2F;www.techrxiv.org&#x2F;users&#x2F;717330&#x2F;articles&#x2F;702287-on-fer...</a>

Next target: the Langlands program ?