3 ms·

Well, it appears that Kevin Buzzard hasn't fully made up his mind on this point (from the presentation by him that I linked): > If my work in pure mathematics

by t_mann 3y ago

Well, it appears that Kevin Buzzard hasn't fully made up his mind on this point (from the presentation by him that I linked): > If my work in pure mathematics is neither useful nor 100 percent guaranteed to be correct, it is surely a waste of time. So I have decided to stop attempting to generate new mathematics, and concentrate instead on carefully checking "known" mathematics on a computer I also remember him saying sth along the lines that his concern about how much of recent math is reliable being a major inspiration for his initial involvement in an interview (could have been for Quanta Magazine or so), but couldn't find it now, so can't verify.

staunton 3y ago
That's actually quite interesting. I hadn't read the entire presentation, to be honest. Maybe it's a case of communicating priorities differently to different stakeholders... After all, it's about what the primary motivation is. Aside from that, the statement you're quoting is deeply puzzling to me. No work is ever "100% guaranteed to be correct", not even something formally verified by a computer, so that statement is either false, vacuous concerning correctness or he didn't mean it literally... (Maybe 100% really means 99.99999% of the time, or something)
- t_mann 3y ago
  Not clear to me from when the chat statement is, but given that the presentation is from 2020, it would actually be funny if he went from 'this is going to get us 100% certainty' to 'well, we might never be fully sure, but at least it's a cool library'. Jokes aside, I'm pretty sure he was aware of the limitations at all times, and I'm reading this statement in the context of his examples in the presentation. There's a nice story in a Quanta interview about how he was approached by Peter Scholze to help formalize part of a proof. Scholze had asked whether they'd gone through his recent work, and when he said Yes, Scholze asked whether they'd carefully checked theorem 9.1. Buzzard said no, they didn't have enough time left when they got to chapter 9. And Scholze said, see, that's the problem, is anyone in the world really going to check 9.1? And then there are the stories in the presentation, where entire published proofs are put in question, not because of any direct mistake by the authors, but because of a problem in a lemma they used from previous work. This kind of transitive dependency chain could go down multiple papers, and there's really no guarantee that the later results are salvageable. So it seems to me that formalization would be a great practical tool to mitigate those problems. And then yes, it's also super cool in its own right (imho), just the fact of collecting the knowledge, and then the related work might also prove useful for formal verification (of hard/software systems), which has practical relevance, and mathlib might also just happen to become a great enabler for developing math-focused AI. So lots of good reasons to do it, but correctness might still be the most direct payoff: Terry Tao has a different blog post about how he found a (fixable) error in a recent proof of his, thanks to Lean. If that happens to him on one of the first occasions where he uses the tool seriously, then we can only guess what's waiting to be fixed (or thrown out) in the whole body of published mathematics.
  - staunton 3y ago
    I would strongly assume Buzzard believes those two positions to be perfectly compatible and consistent. I'm sure it would be very insightful to hear him explain how they are. Hope someone asks him about it. > formalization would be a great practical tool to mitigate those problems Yes, I agree. V. Voevodsky's story is a great example how things can go wrong and I very much admire him for the consequences he took from that. However, if some mathematician has the goal of advancing a certain field, I don't think you can argue convincingly in 2023 that they should formalize their papers because making extra sure there's no errors is worth the time investment in terms of advancing the field. Again, I expect to see this slowly change.
    - t_mann 3y ago
      I'm not saying that starting 2024, journals should only start accepting formalized proofs. I'm well aware that we're probably many thousands of person years away from being able to formalize research involving modern mathematical objects like rough paths or perfectoid spaces. But I do think that we should be moving in that direction. We're halfway through formalizing undergrad education, once we're there we could start including it in graduate courses, and at some point we'll have caught up. Many thousands of years of work divided by many thousands of active grad students maybe isn't prohibitively much. I don't see a reason why in some future, something like Lean couldn't replace something like LaTeX as the de-facto standard language for communicating mathematics. We could build the papers directly from source with docstrings. I don't even think that it would replace peer review, since this considers at least three things, correctness, novelty and relevance, roughly in that order, but it could make it substantially easier by automating much of the first part. And I think it might make the paper writing itself more efficient and enjoyable as well.

by t_mann 3y ago

staunton 3y ago

That's actually quite interesting. I hadn't read the entire presentation, to be honest. Maybe it's a case of communicating priorities differently to different stakeholders... After all, it's about what the primary motivation is. Aside from that, the statement you're quoting is deeply puzzling to me. No work is ever "100% guaranteed to be correct", not even something formally verified by a computer, so that statement is either false, vacuous concerning correctness or he didn't mean it literally... (Maybe 100% really means 99.99999% of the time, or something)

t_mann 3y ago
Not clear to me from when the chat statement is, but given that the presentation is from 2020, it would actually be funny if he went from 'this is going to get us 100% certainty' to 'well, we might never be fully sure, but at least it's a cool library'. Jokes aside, I'm pretty sure he was aware of the limitations at all times, and I'm reading this statement in the context of his examples in the presentation. There's a nice story in a Quanta interview about how he was approached by Peter Scholze to help formalize part of a proof. Scholze had asked whether they'd gone through his recent work, and when he said Yes, Scholze asked whether they'd carefully checked theorem 9.1. Buzzard said no, they didn't have enough time left when they got to chapter 9. And Scholze said, see, that's the problem, is anyone in the world really going to check 9.1? And then there are the stories in the presentation, where entire published proofs are put in question, not because of any direct mistake by the authors, but because of a problem in a lemma they used from previous work. This kind of transitive dependency chain could go down multiple papers, and there's really no guarantee that the later results are salvageable. So it seems to me that formalization would be a great practical tool to mitigate those problems. And then yes, it's also super cool in its own right (imho), just the fact of collecting the knowledge, and then the related work might also prove useful for formal verification (of hard/software systems), which has practical relevance, and mathlib might also just happen to become a great enabler for developing math-focused AI. So lots of good reasons to do it, but correctness might still be the most direct payoff: Terry Tao has a different blog post about how he found a (fixable) error in a recent proof of his, thanks to Lean. If that happens to him on one of the first occasions where he uses the tool seriously, then we can only guess what's waiting to be fixed (or thrown out) in the whole body of published mathematics.
- staunton 3y ago
  I would strongly assume Buzzard believes those two positions to be perfectly compatible and consistent. I'm sure it would be very insightful to hear him explain how they are. Hope someone asks him about it. > formalization would be a great practical tool to mitigate those problems Yes, I agree. V. Voevodsky's story is a great example how things can go wrong and I very much admire him for the consequences he took from that. However, if some mathematician has the goal of advancing a certain field, I don't think you can argue convincingly in 2023 that they should formalize their papers because making extra sure there's no errors is worth the time investment in terms of advancing the field. Again, I expect to see this slowly change.
  - t_mann 3y ago
    I'm not saying that starting 2024, journals should only start accepting formalized proofs. I'm well aware that we're probably many thousands of person years away from being able to formalize research involving modern mathematical objects like rough paths or perfectoid spaces. But I do think that we should be moving in that direction. We're halfway through formalizing undergrad education, once we're there we could start including it in graduate courses, and at some point we'll have caught up. Many thousands of years of work divided by many thousands of active grad students maybe isn't prohibitively much. I don't see a reason why in some future, something like Lean couldn't replace something like LaTeX as the de-facto standard language for communicating mathematics. We could build the papers directly from source with docstrings. I don't even think that it would replace peer review, since this considers at least three things, correctness, novelty and relevance, roughly in that order, but it could make it substantially easier by automating much of the first part. And I think it might make the paper writing itself more efficient and enjoyable as well.