33 ms·

Fermat's Last Theorem – how it’s going

443 points by verbify 2y ago

TechPlasma 2y ago
[flagged]
- dboreham 2y ago
  42 surely?
  - olddustytrail 2y ago
    I can only count to 4.
munchler 2y ago
> 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. 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.
- FredPret 2y ago
  Compilers have this very same habit!
  - munchler 2y ago
    Yes. In fact, Lean is a compiler and type checkers are theorem provers (by the Curry-Howard correspondence). Proofs are programs!
    - dboreham 2y ago
      And Mathematics is Computer Science. Took me most of a lifetime to realize this.
      - pkoird 2y ago
        I'd argue for the converse: Computer Science is Mathematics
        practal 2y ago
        Let's just say there is a really big overlap between the two. And each one can learn from the point of view of the other.
        hughesjj 2y ago
        Then we have the ghosts of information and category theories underpinning/influencing them all (including physics) (to some degree)
        naasking 2y ago
        > I'd argue for the converse: Computer Science is Mathematics The space of programs is arguably larger than the space of mathematical systems, because programs can be logically inconsistent. This suggests that mathematics is a logically consistent subset of computer science, not the other way around.
        anthk 2y ago
        And then you are wrong because everything now theorized into CS was already a thing in Math since long ago. Lisp? Knuth and computation? Lambda Calculus did it before. ] https://en.m.wikipedia.org/wiki/Lambda_calculus https://en.m.wikipedia.org/wiki/Lambda_calculus And, before computers, we had these: https://en.m.wikipedia.org/wiki/State_machine https://en.m.wikipedia.org/wiki/State_machine https://en.m.wikipedia.org/wiki/Control_theory https://en.m.wikipedia.org/wiki/Control_theory
      - gedpeck 2y ago
- deleted 2y ago
  [deleted]
pennomi 2y ago
I’m happy to see so much work going into fixing human errors in mathematics in a rigorous way.
seanwilson 2y ago
> 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. It makes me think about how you get UI/UX/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/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/or the designer will have to patch somehow. 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.
- coliveira 2y ago
  > consider getting mathematics written down properly, i.e. in a formal system This was already tried, and failed (Hilbert). In the aftermath of the failure we learned that mathematics cannot be completely formalized. So this points to a fundamental problem with using AI to do math.
  - hansvm 2y ago
    TFA isn't about AI; it's about taking the same arguments mathematicians are already writing down semi-formally with a hand-wavy argument that it could be made completely formal, and instead/also writing them down formally. In cases where the Hilbert machine applies, the mathematician writing down the semi-formal argument already has to state the new axioms, justify them, and reason about how they apply, and the proposal would just take that "reason about how they apply" step and write it in a computer-verifiable way.
bee_rider 2y ago
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. Oh well, hopefully when they get the machines to solve math, they’ll still want them to run a couple percents faster every year.
- Etheryte 2y ago
  [flagged]
  - analog31 2y ago
    While true, there are some clues such as the correlation between someone's occupation and their IQ.
  - bee_rider 2y ago
    I just meant in the context of math skills, but I definitely acknowledge that it was poor phrasing on my part.
    - dogboat 2y ago
      On the other hand get them to try and debug code. And then you might realize the redicilous amount of unwritten lore that software engineering has. OTOH software engineering has courses but you need to work with people to get good not just read books. Like math.
  - TechDebtDevin 2y ago
    I don't even understand how you interpreted that to have anything to do with being "smarter or making more money". Get some more coffee dude.
    - dogboat 2y ago
      Maybe less coffee :)
lincolnq 2y ago
If you're interested in this stuff at all, check out some code. Example: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M... Also check out the blueprint, which describes the overall structure of the code: https://imperialcollegelondon.github.io/FLT/blueprint/ https://imperialcollegelondon.github.io/FLT/blueprint/ I'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's no need for unittests (or, in some sense, the final proof statement is the unittest) :P
- staunton 2y ago
  Most (larger) Lean projects still have "unit tests". Those might be, e.g., trivial examples and counter examples to some definition, to make sure it isn't vacuous.
  - schoen 2y ago
    That's such a nice way to think about unit tests! (In this context and others.)
  - pierrefermat1 2y ago
    I think the better mapping of unit tests would actually be proofs of lemmas ?
    - staunton 2y ago
      I don't see why you would think that. In such a project theorems and proofs are "the main point of the software". The unit tests make sure certain things don't go wrong by noticing when developers, e.g., mess up while refacing something. Also, people actually put the things I was talking about in a folder called "test"...
ur-whale 2y ago
This article makes me very happy. One of the many reasons I love math is the feeling I've always had that with it, we're building skyscraper-sized mental structures that are built on provably indestructible foundations. With the advent of "modern" 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. Examples: graph coloring theorem, Fermat's last theorem, finite group classification theorem ... all of them with gigantic proofs, out of reach of most casual observers. And lo and behold, someone found shaky stuff in a long proof, what a surprise. 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 ! [1] https://en.wikipedia.org/wiki/Shinichi_Mochizuki https://en.wikipedia.org/wiki/Shinichi_Mochizuki
Retr0id 2y ago
This makes me wonder if there'll ever be a significant bug discovered in Lean itself, breaking past formalisation work.
- pkoird 2y ago
  Ahh, so maybe we should first focus on formalizing Lean itself?
  - digama0 2y ago
    Should I introduce you to https://arxiv.org/abs/2403.14064 https://arxiv.org/abs/2403.14064 ?
- moomin 2y ago
  For the problem to affect proofs, it would have to be in the type checker, and the type system isn’t really that complex. The good news is that every single user of Lean checks this works every day. Finding a flaw that literally everyone relies upon and doesn’t notice is pretty implausible.
- munchler 2y ago
  Lean has a small “kernel” that has been independently checked multiple times, and the rest of Lean depends on the kernel. A soundness bug is still possible, but pretty unlikely at this point. https://lean-lang.org/lean4/doc/faq.html https://lean-lang.org/lean4/doc/faq.html
  - norlygfyd 2y ago
    Soundness of Lean requires more than correctness of the kernel - it requires that the theory be sound. That, frankly, is a matter of mathematics folklore. "It is known" that the combination of rules Lean uses is sound... unless it isn't.
    - munchler 2y ago
      That would be a bug in math itself, rather than a bug in Lean. It's possible, of course, but even less likely.
vouaobrasil 2y ago
> 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. 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 "skip the details". 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't easily be found in the literature. It's only when such a person writes a book explaining everything that it might be possible, and sometimes not even then. The truth is, a lot of modern math is on shaky ground when it comes to stuff written down.
- uffjedn 2y ago
  Studied math a long time ago and one of my profs was proud about not going into the details. He said "Once you did something 100 times, you can go and say -as easily observable- and move on."
  - brobdingnagians 2y ago
    I loved that some of the proof solutions in the back of mathematical logic book said, "Observe that ..." as the start of the proof. Our little study group definitely did not see how what followed was an observation we would have made.
    - moomin 2y ago
      Baker's little book of number theory made me work to get through every page...
  - inglor_cz 2y ago
    I was an algebra major at the turn of the century and I hated that attitude. For the prof, yeah, easily observable. What about the students who try to absorb that particular article? You already have to balance the main topic in your brain, and you get these extra distractions on top of it.
boothby 2y ago
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, "well, no, I'd much rather find a counterexample." The crowd went wild; I've never made a group of experts so angry as that day. 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't understand the definitions, I certainly knew them and understood the notation. But there'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? 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 "native tongue." 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.
- bell-cot 2y ago
  > The crowd went wild; I've never made a group of experts so angry as... Also not a number theorist...but I'd bet those so-called experts had invested far, far too many of their man-years in that unproven conjecture. All of which effort and edifice would collapse into the dumpster if some snot-nosed little upstart like you, using crude computation, achieved overnight fame by finding a counter-example. (If I could give my many-decades-ago younger self some advice for math grad school, one bit of that would be: For any non-trivial "Prove X" assignment, start by spending at least 1/4 of my time budget looking for counter-examples. For academic assignments, that's 99% likely to fail. But the insight you'll get into the problem by trying will be more worth it. And the other 1% of the time you'll look like a genius. And - as soon as you attempt real math research, those odds shift enormously, in favor of the counterexample-first approach.)
graycat 2y ago
This thread seems to be about good writing for math. Okay, for some decades, I've read, written, taught, applied, and published, in total, quite a lot of math. Got a Ph.D. in applied math. Yes, there are problems in writing math, that is, some math is poorly written. 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. For more, carefully reading some well-written math can help learning how to write math well: Paul R.\ Halmos, {\it Finite-Dimensional Vector Spaces, Second Edition,\/} D.\ Van Nostrand Company, Inc., Princeton, New Jersey, 1958.\ \ R.\ Creighton Buck, {\it Advanced Calculus,\/} McGraw-Hill, New York, 1956.\ \ Tom M.\ Apostol, {\it Mathematical Analysis: Second Edition,\/} ISBN 0-201-00288-4, Addison-Wesley, Reading, Massachusetts, 1974.\ \ H.\ L.\ Royden, {\it Real Analysis: Second Edition,\/} Macmillan, New York, 1971.\ \ Walter Rudin, {\it Real and Complex Analysis,\/} ISBN 07-054232-5, McGraw-Hill, New York, 1966.\ \ Leo Breiman, {\it Probability,\/} ISBN 0-89871-296-3, SIAM, Philadelphia, 1992.\ \ Jacques Neveu, {\it Mathematical Foundations of the Calculus of Probability,\/} Holden-Day, San Francisco, 1965.\ \
- jhanschoo 2y ago
  This isn't just about good writing for math; the post author was trying to verify FLT as is developed in the literature, and along the way they discovered that a lemma underpinning a whole subfield is untrue, as was used. They nevertheless have confidence that the subfield is largely salvageable, by virtue of the faith that if it were bogus, someone would have already found negative results. But now they had to find a suitable replacement to underpin the field.
ykonstant 2y ago
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. 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/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). Also, like Loeffler in the comments, I don't trust the "people have been using crystalline cohomology forever without trouble" 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). But precisely because of that, large swathes of the theory will be correct. Errors will 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.
- cobbal 2y ago
  One of the best things about proof assistants is that they're not convinced by how "obvious" you think something is. It's much harder for a human to resist proof by social forces such as intimidation, confidence, and "it's well known".
- zyklu5 2y ago
  Re: that dig at 4-manifolds Are you aware of the book on [The Disc Embedding Theorem](https://academic.oup.com/book/43693 https://academic.oup.com/book/43693) based on 12 lectures Freedman gave roughly a decade ago.
  - ykonstant 2y ago
    No, I am not an expert of 4-manifold theory and would not really understand most of the chapters. If this book fixes some of the literature issues in that field that is amazing! Does it finally resolve the issue of nobody understanding the construction of topological Casson handles? Edit: I see from the MO comments "The fully topological version of the disc embedding theorem is beyond the scope of this book, since we will not discuss Quinn's proof of transversality."
modeless 2y ago
> 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. I'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?
- staunton 2y ago
  This has happened before, see, e.g. the biography of Vladimir Voevodsky. Spoiler: the world kept spinning.
  - moomin 2y ago
    Russell’s paradox did the same thing. They had to go back to the drawing board.
- bubblyworld 2y ago
  I think it depends how widely used that branch of maths becomes. In fact, I'd say that the word "branch" is a bit misleading - for many theories it's much more of a "knot", with influences tying them to many many other theories across the mathematical landscape. And those theories are themselves tied to others, etcetera. It would be a very strange situation if the foundation fell apart logically without any ramifications in the rest of this "knot". A huge swathe of free-floating mathematics that's completely internally consistent but for this one error? Difficult to imagine for me in the case of cohomology from the article. I guess strictly speaking this is more of a philosophical stance - I like to believe that a lot of the current mathematics has been discovered "naturally" in some sense =)
- rocqua 2y ago
  People hunt for counter examples to proofs they are working on. If the basis of their work is wrong, it's quite possible for one of the counter examples to also disprove the base theorem. So building on a faulty foundation is likely to reveal faults in the foundation. Similarly, once in a while math gets applied and is used to make predictions. When the math is wrong, those predictions are wrong. And those wrong predictions draw a lot of attention.
moomin 2y ago
I remember when I was a student a friend of mine telling me this guy was giving a seminar and he'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. All of which is a long way of saying the line "the old-fashioned 1990s proof" makes me feel _really_ old.
- rateofclimb 2y ago
  As a CS undergrad at Berkeley in the 90's I took an upper division math class in which we worked through the "old school" proof which was brand new and exciting then. Pretty much everyone else in the class was a math grad student. I don't think I understood more than 20% of the material! :)
  - williamstein 2y ago
    I took that class with you! It was amazing. Here are my notes: https://wstein.org/books/ribet-stein/ https://wstein.org/books/ribet-stein/
    - williamstein 2y ago
      And the professor who taught that course won a major prize today: Ribet to Receive 2025 AMS Steele Prize for Seminal Research - https://www.ams.org/news?news_id=7391&fbclid=IwZXh0bgNhZW0CMTEAAR2d6t_wCPkea3MpJZWld6JyhIKeMcTuivQEkZ3tTXeGBZM-32jxKrpq4_4_aem_7-o00iW2IS_Z8yS9JVhQRA https://www.ams.org/news?news_id=7391&fbclid=IwZXh0bgNhZW0CM...
    - rateofclimb 2y ago
      Thanks for sharing that! Very cool.
- dogboat 2y ago
  There was a great documentary TV shown about this story.
baruz 2y ago
This is the the talk by Dr de Frutos—Fernandez that Dr Buzzard mentions at the end: https://m.youtube.com/watch?v=QCRLwC5JQw0 https://m.youtube.com/watch?v=QCRLwC5JQw0
EmberJune46 2y ago
[dead]
tunesmith 2y ago
Haha, that author is a funny writer. Very weird experience for that to be so readable, when I didn't understand probably half the content. 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: 'vitiated'. The conclusion might still be true, it just needs a new or repaired proof; the initial proof is 'vitiated'. I like how the word sounds, too.
- euroderf 2y ago
  Perhaps more delightful to the ears to hear that a proof has been disemboweled.
MrMcCall 2y ago
One of my favorite Horizon episodes is the FLT one that features Prof. Andrew Wiles' development of his proof (I have watched it many times). Of course, it is grounded in Fermat's margin note about his having a wonderful proof that couldn't fit in said margin. At the end of the documentary, the various mathematicians in it note that AW's proof certaintly wasn't what PdF had in mind because AW's proof is thorougly modern. So I have wondered about PdF's possible thinking. Now, the degenerate case of n=2 is just the Pythagorean Theorem c^2 = a^2 + b^2 and we now know from AW's proof that the cubic and beyond fail. Now, the PT is successful because the square b^2 can be "squished" over the corner of a^2, leaving a perfect square c^2. [Let's let the a^n part be the bigger of the two.] 5^2 = 4^2 + 3^2 25 = 16 + 9 25 = 16 + (4 + 4 + 1) Each of the 4's go on the sides, and the 1 goes on the corner, leaving a pure 5x5 square left over. Now, for cubes, we now know that a cube cannot be "squished" onto another cube's corner in such a way that makes a bigger cube. I'm not up for breaking out my (diminishing) algebra right now (as it'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. 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't work, leads me to wonder if this is an interesting approach. It also makes me curious to know why it isn't, if that is indeed the case, (which I assume is probable). As to the n=4 and beyond, I would just hand-wave them away and say something like, "Well, of course they are more fractally impossible", which by that I mean that a real mathematician would have to say exactly why the n=3 case failing means that the n>=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.) 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. I would enjoy learning why I'm so utterly wrong about this, but I found it a fun mental exercise some years ago that's been swimming around in my brain. Thanks in advance if there are any takers around here. :-) [And, my favorite Horizon episode is 'Freak Wave'.]
- jovas 2y ago
  I believe Wiles' proof requires the case of n=3 (Euler), and n=4 (Fermat) separately. That is, Wiles' proof starts with n=5 for nontrivial reasons. So it is more likely that Fermat saw n=4, and thought the rest would be similar.
sam_goody 2y ago
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. I don'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. But now I wonder that he didn't hit dozens or hundreds of errors over the years.
- hughesjj 2y ago
  I'd be careful taking anything from "surely you're joking" as a fact btw. There's a good popsci comms video on why here https://youtu.be/TwKpj2ISQAc?si=bpZOBy9WBGQzi6sk https://youtu.be/TwKpj2ISQAc?si=bpZOBy9WBGQzi6sk
  - j16sdiz 2y ago
    She is more like complaining some (most?) RPF "bros" act like jerks, emotionally unstable, etc. I guess the same can be said about many other "fanboi", and have little to do with the facts in the book
    - hughesjj 2y ago
      No, she's claiming that most of those stories were made up by a third guy with Daddy issues (if you want to be reductive)
- blackenedgem 2y ago
  You may want to watch this if Surely You're Joking read years ago is your main reference point: https://youtu.be/TwKpj2ISQAc https://youtu.be/TwKpj2ISQAc
jebarker 2y ago
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?
- ted_dunning 2y ago
  It is also utterly unlike in that the formalization of math actually has real impact. Cyc has never had any impact and almost certainly never will.
- practal 2y ago
  Yes.
- zozbot234 2y ago
  If anything, it's a relatively straightforward way to do what amounts to publishable work in mathematics. Besides the obvious point of being able to claim "I've dotted all the i's and crossed all the t's", formalized proofs are often more elegant than the original they're based on because refactoring a proof to be simpler, more general etc. and checking that it still goes through is comparatively easy - and obviously, mathematicians are interested in that.
  - jebarker 2y ago
    The refactoring idea is interesting because I can imagine "proof compression" creating a less readable proof too, similarly to how a code one liner can be harder to read.
charlieyu1 2y ago
What is the simplest proof of FLT these days? I don’t think elementary proofs exist
levn11 2y ago
https://www.techrxiv.org/users/717330/articles/702287-on-fermat-s-last-theorem https://www.techrxiv.org/users/717330/articles/702287-on-fer...
Tainnor 2y ago
For the past year or so, I'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's because I insisted on defining the complex numbers, (power) series, exp and sin "from scratch", even though they're of course already in mathlib. Many of my troubles probably come from the fact that I only have a BSc in maths and that I'm not very familiar with Lean/mathlib and don'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). In terms of proof automation, I believe we're not there yet. There are too many things that are absolutely harder to prove than they should be (although I'm sure that there's also a lot of tricks that I'm just not aware of). My biggest gripe concerns casts, in "regular" 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're different types with an injective map / 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 "stacks" of casts, e.g. a natural number cast to a real cast to a complex number etc. 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. [0] This is technically only true for sentences without existential quantifiers.
- digama0 2y ago
  If this is your situation, you should absolutely be asking more questions on Zulip. It is really easy to get guidance on how to use mathlib, what things exist and where they are. The issue with stacked casts is mostly solved by the `norm_cast` tactic. Again, ask more questions on Zulip - even if you don't ask about this in particular, if you suggest it in passing, or your code gives indications of an unnecessarily complicated proof style, you will get suggestions about tactics you may not be aware of. One way you can focus a question like this if you don't know what techniques to use but just have a feeling that formalization is too hard, is to isolate an example where you really had to work hard to get a proof and your proof is unsatisfying to you, and challenge people to golf it down. These kind of questions are generally well received and everyone learns a lot from them.
naasking 2y ago
Nice story, and I'm glad formalization work is proceeding. "Details left as an exercise to the reader" is the bane of true knowledge.
euroderf 2y ago
Next target: the Langlands program ?
ThomasBb 2y ago
Someone had to post this video of a song about Fermat - even if it’s in Dutch - legend: https://youtu.be/X2AVi6RCgN8?si=ZnN9lMb-XuirZ20_ https://youtu.be/X2AVi6RCgN8?si=ZnN9lMb-XuirZ20_
le-mark 2y ago
When this topic comes up I love sharing this talk by Sussman; because every time I watch it again! https://www.infoq.com/presentations/Expression-of-Ideas/ https://www.infoq.com/presentations/Expression-of-Ideas/

443 points by verbify 2y ago

TechPlasma 2y ago

[flagged]

dboreham 2y ago
42 surely?
- olddustytrail 2y ago
  I can only count to 4.

munchler 2y ago

> 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. 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.

FredPret 2y ago
Compilers have this very same habit!
- munchler 2y ago
  Yes. In fact, Lean is a compiler and type checkers are theorem provers (by the Curry-Howard correspondence). Proofs are programs!
  - dboreham 2y ago
    And Mathematics is Computer Science. Took me most of a lifetime to realize this.
    - pkoird 2y ago
      I'd argue for the converse: Computer Science is Mathematics
      - practal 2y ago
        Let's just say there is a really big overlap between the two. And each one can learn from the point of view of the other.
        hughesjj 2y ago
        Then we have the ghosts of information and category theories underpinning/influencing them all (including physics) (to some degree)
      - naasking 2y ago
        > I'd argue for the converse: Computer Science is Mathematics The space of programs is arguably larger than the space of mathematical systems, because programs can be logically inconsistent. This suggests that mathematics is a logically consistent subset of computer science, not the other way around.
        anthk 2y ago
        And then you are wrong because everything now theorized into CS was already a thing in Math since long ago. Lisp? Knuth and computation? Lambda Calculus did it before. ] https://en.m.wikipedia.org/wiki/Lambda_calculus https://en.m.wikipedia.org/wiki/Lambda_calculus And, before computers, we had these: https://en.m.wikipedia.org/wiki/State_machine https://en.m.wikipedia.org/wiki/State_machine https://en.m.wikipedia.org/wiki/Control_theory https://en.m.wikipedia.org/wiki/Control_theory
    - gedpeck 2y ago
deleted 2y ago
[deleted]

pennomi 2y ago

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

seanwilson 2y ago

> 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. It makes me think about how you get UI/UX/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/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/or the designer will have to patch somehow. 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.

coliveira 2y ago
> consider getting mathematics written down properly, i.e. in a formal system This was already tried, and failed (Hilbert). In the aftermath of the failure we learned that mathematics cannot be completely formalized. So this points to a fundamental problem with using AI to do math.
- hansvm 2y ago
  TFA isn't about AI; it's about taking the same arguments mathematicians are already writing down semi-formally with a hand-wavy argument that it could be made completely formal, and instead/also writing them down formally. In cases where the Hilbert machine applies, the mathematician writing down the semi-formal argument already has to state the new axioms, justify them, and reason about how they apply, and the proposal would just take that "reason about how they apply" step and write it in a computer-verifiable way.

bee_rider 2y ago

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. Oh well, hopefully when they get the machines to solve math, they’ll still want them to run a couple percents faster every year.

Etheryte 2y ago
[flagged]
- analog31 2y ago
  While true, there are some clues such as the correlation between someone's occupation and their IQ.
- bee_rider 2y ago
  I just meant in the context of math skills, but I definitely acknowledge that it was poor phrasing on my part.
  - dogboat 2y ago
    On the other hand get them to try and debug code. And then you might realize the redicilous amount of unwritten lore that software engineering has. OTOH software engineering has courses but you need to work with people to get good not just read books. Like math.
- TechDebtDevin 2y ago
  I don't even understand how you interpreted that to have anything to do with being "smarter or making more money". Get some more coffee dude.
  - dogboat 2y ago
    Maybe less coffee :)

lincolnq 2y ago

If you're interested in this stuff at all, check out some code. Example: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M... Also check out the blueprint, which describes the overall structure of the code: https://imperialcollegelondon.github.io/FLT/blueprint/ https://imperialcollegelondon.github.io/FLT/blueprint/ I'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's no need for unittests (or, in some sense, the final proof statement is the unittest) :P

staunton 2y ago
Most (larger) Lean projects still have "unit tests". Those might be, e.g., trivial examples and counter examples to some definition, to make sure it isn't vacuous.
- schoen 2y ago
  That's such a nice way to think about unit tests! (In this context and others.)
- pierrefermat1 2y ago
  I think the better mapping of unit tests would actually be proofs of lemmas ?
  - staunton 2y ago
    I don't see why you would think that. In such a project theorems and proofs are "the main point of the software". The unit tests make sure certain things don't go wrong by noticing when developers, e.g., mess up while refacing something. Also, people actually put the things I was talking about in a folder called "test"...

ur-whale 2y ago

This article makes me very happy. One of the many reasons I love math is the feeling I've always had that with it, we're building skyscraper-sized mental structures that are built on provably indestructible foundations. With the advent of "modern" 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. Examples: graph coloring theorem, Fermat's last theorem, finite group classification theorem ... all of them with gigantic proofs, out of reach of most casual observers. And lo and behold, someone found shaky stuff in a long proof, what a surprise. 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 ! [1] https://en.wikipedia.org/wiki/Shinichi_Mochizuki https://en.wikipedia.org/wiki/Shinichi_Mochizuki

Retr0id 2y ago

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

pkoird 2y ago
Ahh, so maybe we should first focus on formalizing Lean itself?
- digama0 2y ago
  Should I introduce you to https://arxiv.org/abs/2403.14064 https://arxiv.org/abs/2403.14064 ?
moomin 2y ago
For the problem to affect proofs, it would have to be in the type checker, and the type system isn’t really that complex. The good news is that every single user of Lean checks this works every day. Finding a flaw that literally everyone relies upon and doesn’t notice is pretty implausible.
munchler 2y ago
Lean has a small “kernel” that has been independently checked multiple times, and the rest of Lean depends on the kernel. A soundness bug is still possible, but pretty unlikely at this point. https://lean-lang.org/lean4/doc/faq.html https://lean-lang.org/lean4/doc/faq.html
- norlygfyd 2y ago
  Soundness of Lean requires more than correctness of the kernel - it requires that the theory be sound. That, frankly, is a matter of mathematics folklore. "It is known" that the combination of rules Lean uses is sound... unless it isn't.
  - munchler 2y ago
    That would be a bug in math itself, rather than a bug in Lean. It's possible, of course, but even less likely.

vouaobrasil 2y ago

> 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. 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 "skip the details". 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't easily be found in the literature. It's only when such a person writes a book explaining everything that it might be possible, and sometimes not even then. The truth is, a lot of modern math is on shaky ground when it comes to stuff written down.

uffjedn 2y ago
Studied math a long time ago and one of my profs was proud about not going into the details. He said "Once you did something 100 times, you can go and say -as easily observable- and move on."
- brobdingnagians 2y ago
  I loved that some of the proof solutions in the back of mathematical logic book said, "Observe that ..." as the start of the proof. Our little study group definitely did not see how what followed was an observation we would have made.
  - moomin 2y ago
    Baker's little book of number theory made me work to get through every page...
- inglor_cz 2y ago
  I was an algebra major at the turn of the century and I hated that attitude. For the prof, yeah, easily observable. What about the students who try to absorb that particular article? You already have to balance the main topic in your brain, and you get these extra distractions on top of it.

boothby 2y ago

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, "well, no, I'd much rather find a counterexample." The crowd went wild; I've never made a group of experts so angry as that day. 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't understand the definitions, I certainly knew them and understood the notation. But there'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? 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 "native tongue." 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.

bell-cot 2y ago
> The crowd went wild; I've never made a group of experts so angry as... Also not a number theorist...but I'd bet those so-called experts had invested far, far too many of their man-years in that unproven conjecture. All of which effort and edifice would collapse into the dumpster if some snot-nosed little upstart like you, using crude computation, achieved overnight fame by finding a counter-example. (If I could give my many-decades-ago younger self some advice for math grad school, one bit of that would be: For any non-trivial "Prove X" assignment, start by spending at least 1/4 of my time budget looking for counter-examples. For academic assignments, that's 99% likely to fail. But the insight you'll get into the problem by trying will be more worth it. And the other 1% of the time you'll look like a genius. And - as soon as you attempt real math research, those odds shift enormously, in favor of the counterexample-first approach.)

graycat 2y ago

This thread seems to be about good writing for math. Okay, for some decades, I've read, written, taught, applied, and published, in total, quite a lot of math. Got a Ph.D. in applied math. Yes, there are problems in writing math, that is, some math is poorly written. 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. For more, carefully reading some well-written math can help learning how to write math well: Paul R.\ Halmos, {\it Finite-Dimensional Vector Spaces, Second Edition,\/} D.\ Van Nostrand Company, Inc., Princeton, New Jersey, 1958.\ \ R.\ Creighton Buck, {\it Advanced Calculus,\/} McGraw-Hill, New York, 1956.\ \ Tom M.\ Apostol, {\it Mathematical Analysis: Second Edition,\/} ISBN 0-201-00288-4, Addison-Wesley, Reading, Massachusetts, 1974.\ \ H.\ L.\ Royden, {\it Real Analysis: Second Edition,\/} Macmillan, New York, 1971.\ \ Walter Rudin, {\it Real and Complex Analysis,\/} ISBN 07-054232-5, McGraw-Hill, New York, 1966.\ \ Leo Breiman, {\it Probability,\/} ISBN 0-89871-296-3, SIAM, Philadelphia, 1992.\ \ Jacques Neveu, {\it Mathematical Foundations of the Calculus of Probability,\/} Holden-Day, San Francisco, 1965.\ \

jhanschoo 2y ago
This isn't just about good writing for math; the post author was trying to verify FLT as is developed in the literature, and along the way they discovered that a lemma underpinning a whole subfield is untrue, as was used. They nevertheless have confidence that the subfield is largely salvageable, by virtue of the faith that if it were bogus, someone would have already found negative results. But now they had to find a suitable replacement to underpin the field.

ykonstant 2y ago

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. 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/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). Also, like Loeffler in the comments, I don't trust the "people have been using crystalline cohomology forever without trouble" 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). But precisely because of that, large swathes of the theory will be correct. Errors will 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.

cobbal 2y ago
One of the best things about proof assistants is that they're not convinced by how "obvious" you think something is. It's much harder for a human to resist proof by social forces such as intimidation, confidence, and "it's well known".
zyklu5 2y ago
Re: that dig at 4-manifolds Are you aware of the book on [The Disc Embedding Theorem](https://academic.oup.com/book/43693 https://academic.oup.com/book/43693) based on 12 lectures Freedman gave roughly a decade ago.
- ykonstant 2y ago
  No, I am not an expert of 4-manifold theory and would not really understand most of the chapters. If this book fixes some of the literature issues in that field that is amazing! Does it finally resolve the issue of nobody understanding the construction of topological Casson handles? Edit: I see from the MO comments "The fully topological version of the disc embedding theorem is beyond the scope of this book, since we will not discuss Quinn's proof of transversality."

modeless 2y ago

> 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. I'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?

staunton 2y ago
This has happened before, see, e.g. the biography of Vladimir Voevodsky. Spoiler: the world kept spinning.
- moomin 2y ago
  Russell’s paradox did the same thing. They had to go back to the drawing board.
bubblyworld 2y ago
I think it depends how widely used that branch of maths becomes. In fact, I'd say that the word "branch" is a bit misleading - for many theories it's much more of a "knot", with influences tying them to many many other theories across the mathematical landscape. And those theories are themselves tied to others, etcetera. It would be a very strange situation if the foundation fell apart logically without any ramifications in the rest of this "knot". A huge swathe of free-floating mathematics that's completely internally consistent but for this one error? Difficult to imagine for me in the case of cohomology from the article. I guess strictly speaking this is more of a philosophical stance - I like to believe that a lot of the current mathematics has been discovered "naturally" in some sense =)
rocqua 2y ago
People hunt for counter examples to proofs they are working on. If the basis of their work is wrong, it's quite possible for one of the counter examples to also disprove the base theorem. So building on a faulty foundation is likely to reveal faults in the foundation. Similarly, once in a while math gets applied and is used to make predictions. When the math is wrong, those predictions are wrong. And those wrong predictions draw a lot of attention.

moomin 2y ago

I remember when I was a student a friend of mine telling me this guy was giving a seminar and he'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. All of which is a long way of saying the line "the old-fashioned 1990s proof" makes me feel _really_ old.

rateofclimb 2y ago
As a CS undergrad at Berkeley in the 90's I took an upper division math class in which we worked through the "old school" proof which was brand new and exciting then. Pretty much everyone else in the class was a math grad student. I don't think I understood more than 20% of the material! :)
- williamstein 2y ago
  I took that class with you! It was amazing. Here are my notes: https://wstein.org/books/ribet-stein/ https://wstein.org/books/ribet-stein/
  - williamstein 2y ago
    And the professor who taught that course won a major prize today: Ribet to Receive 2025 AMS Steele Prize for Seminal Research - https://www.ams.org/news?news_id=7391&fbclid=IwZXh0bgNhZW0CMTEAAR2d6t_wCPkea3MpJZWld6JyhIKeMcTuivQEkZ3tTXeGBZM-32jxKrpq4_4_aem_7-o00iW2IS_Z8yS9JVhQRA https://www.ams.org/news?news_id=7391&fbclid=IwZXh0bgNhZW0CM...
  - rateofclimb 2y ago
    Thanks for sharing that! Very cool.
dogboat 2y ago
There was a great documentary TV shown about this story.

baruz 2y ago

This is the the talk by Dr de Frutos—Fernandez that Dr Buzzard mentions at the end: https://m.youtube.com/watch?v=QCRLwC5JQw0 https://m.youtube.com/watch?v=QCRLwC5JQw0

EmberJune46 2y ago

[dead]

tunesmith 2y ago

Haha, that author is a funny writer. Very weird experience for that to be so readable, when I didn't understand probably half the content. 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: 'vitiated'. The conclusion might still be true, it just needs a new or repaired proof; the initial proof is 'vitiated'. I like how the word sounds, too.

euroderf 2y ago
Perhaps more delightful to the ears to hear that a proof has been disemboweled.

MrMcCall 2y ago

One of my favorite Horizon episodes is the FLT one that features Prof. Andrew Wiles' development of his proof (I have watched it many times). Of course, it is grounded in Fermat's margin note about his having a wonderful proof that couldn't fit in said margin. At the end of the documentary, the various mathematicians in it note that AW's proof certaintly wasn't what PdF had in mind because AW's proof is thorougly modern. So I have wondered about PdF's possible thinking. Now, the degenerate case of n=2 is just the Pythagorean Theorem c^2 = a^2 + b^2 and we now know from AW's proof that the cubic and beyond fail. Now, the PT is successful because the square b^2 can be "squished" over the corner of a^2, leaving a perfect square c^2. [Let's let the a^n part be the bigger of the two.] 5^2 = 4^2 + 3^2 25 = 16 + 9 25 = 16 + (4 + 4 + 1) Each of the 4's go on the sides, and the 1 goes on the corner, leaving a pure 5x5 square left over. Now, for cubes, we now know that a cube cannot be "squished" onto another cube's corner in such a way that makes a bigger cube. I'm not up for breaking out my (diminishing) algebra right now (as it'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. 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't work, leads me to wonder if this is an interesting approach. It also makes me curious to know why it isn't, if that is indeed the case, (which I assume is probable). As to the n=4 and beyond, I would just hand-wave them away and say something like, "Well, of course they are more fractally impossible", which by that I mean that a real mathematician would have to say exactly why the n=3 case failing means that the n>=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.) 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. I would enjoy learning why I'm so utterly wrong about this, but I found it a fun mental exercise some years ago that's been swimming around in my brain. Thanks in advance if there are any takers around here. :-) [And, my favorite Horizon episode is 'Freak Wave'.]

jovas 2y ago
I believe Wiles' proof requires the case of n=3 (Euler), and n=4 (Fermat) separately. That is, Wiles' proof starts with n=5 for nontrivial reasons. So it is more likely that Fermat saw n=4, and thought the rest would be similar.

sam_goody 2y ago

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. I don'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. But now I wonder that he didn't hit dozens or hundreds of errors over the years.

hughesjj 2y ago
I'd be careful taking anything from "surely you're joking" as a fact btw. There's a good popsci comms video on why here https://youtu.be/TwKpj2ISQAc?si=bpZOBy9WBGQzi6sk https://youtu.be/TwKpj2ISQAc?si=bpZOBy9WBGQzi6sk
- j16sdiz 2y ago
  She is more like complaining some (most?) RPF "bros" act like jerks, emotionally unstable, etc. I guess the same can be said about many other "fanboi", and have little to do with the facts in the book
  - hughesjj 2y ago
    No, she's claiming that most of those stories were made up by a third guy with Daddy issues (if you want to be reductive)
blackenedgem 2y ago
You may want to watch this if Surely You're Joking read years ago is your main reference point: https://youtu.be/TwKpj2ISQAc https://youtu.be/TwKpj2ISQAc

jebarker 2y ago

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?

ted_dunning 2y ago
It is also utterly unlike in that the formalization of math actually has real impact. Cyc has never had any impact and almost certainly never will.
practal 2y ago
Yes.
zozbot234 2y ago
If anything, it's a relatively straightforward way to do what amounts to publishable work in mathematics. Besides the obvious point of being able to claim "I've dotted all the i's and crossed all the t's", formalized proofs are often more elegant than the original they're based on because refactoring a proof to be simpler, more general etc. and checking that it still goes through is comparatively easy - and obviously, mathematicians are interested in that.
- jebarker 2y ago
  The refactoring idea is interesting because I can imagine "proof compression" creating a less readable proof too, similarly to how a code one liner can be harder to read.

charlieyu1 2y ago

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

levn11 2y ago

https://www.techrxiv.org/users/717330/articles/702287-on-fermat-s-last-theorem https://www.techrxiv.org/users/717330/articles/702287-on-fer...

Tainnor 2y ago

For the past year or so, I'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's because I insisted on defining the complex numbers, (power) series, exp and sin "from scratch", even though they're of course already in mathlib. Many of my troubles probably come from the fact that I only have a BSc in maths and that I'm not very familiar with Lean/mathlib and don'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). In terms of proof automation, I believe we're not there yet. There are too many things that are absolutely harder to prove than they should be (although I'm sure that there's also a lot of tricks that I'm just not aware of). My biggest gripe concerns casts, in "regular" 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're different types with an injective map / 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 "stacks" of casts, e.g. a natural number cast to a real cast to a complex number etc. 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. [0] This is technically only true for sentences without existential quantifiers.

digama0 2y ago
If this is your situation, you should absolutely be asking more questions on Zulip. It is really easy to get guidance on how to use mathlib, what things exist and where they are. The issue with stacked casts is mostly solved by the `norm_cast` tactic. Again, ask more questions on Zulip - even if you don't ask about this in particular, if you suggest it in passing, or your code gives indications of an unnecessarily complicated proof style, you will get suggestions about tactics you may not be aware of. One way you can focus a question like this if you don't know what techniques to use but just have a feeling that formalization is too hard, is to isolate an example where you really had to work hard to get a proof and your proof is unsatisfying to you, and challenge people to golf it down. These kind of questions are generally well received and everyone learns a lot from them.

naasking 2y ago

Nice story, and I'm glad formalization work is proceeding. "Details left as an exercise to the reader" is the bane of true knowledge.

euroderf 2y ago

Next target: the Langlands program ?

ThomasBb 2y ago

Someone had to post this video of a song about Fermat - even if it’s in Dutch - legend: https://youtu.be/X2AVi6RCgN8?si=ZnN9lMb-XuirZ20_ https://youtu.be/X2AVi6RCgN8?si=ZnN9lMb-XuirZ20_

le-mark 2y ago

When this topic comes up I love sharing this talk by Sussman; because every time I watch it again! https://www.infoq.com/presentations/Expression-of-Ideas/ https://www.infoq.com/presentations/Expression-of-Ideas/