3 ms·

> what excuse do mere mortal mathematicians have? As an ardent proponent of formalizing proofs, I still have to disagree with this framing. Mortal mathematicia

> what excuse do mere mortal mathematicians have? As an ardent proponent of formalizing proofs, I still have to disagree with this framing. Mortal mathematicians don't need any excuse not to formalize their stuff. They rather need a reason to do it. One can give lots of reasons but mathematicians often don't know them or don't agree with them. An important point is, for example, to understand that most formalizing effort is not primarily motivated by a desire to make sure there are no errors in the math.

trevyn 3y ago
>most formalizing effort is not primarily motivated by a desire to make sure there are no errors in the math. Is this because the proof author is generally confident that the proof is essentially correct?
- staunton 3y ago
  Here's people who are working on Lean's Mathlib discussing this https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Array.2EanyM.20is.20inconsistent/near/396178821 https://leanprover.zulipchat.com/#narrow/stream/270676-lean4...
t_mann 3y ago
Mathematicians might not like the insinuation, but the best reason to formalize mathematics is indeed to check its correctness: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_buzzard.pdf https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/sli... tl;dr: contradictory stuff even gets published in the likes of Annals of Mathematics, and even top journals are reluctant to retract published proofs that have later been shown to be false (which in itself shouldn't be possible). Like it or not, the reasons for formalizing mathematics abound, and they have a lot to do with the fact that humans are fallible, but mathematics shouldn't be. The incredibly tedious work of tracking down a proof's correctness to the last axiom is, while overwhelming for humans, exactly the kind of work that classical computers excel at.
- staunton 3y ago
  Of course there's mistakes in papers. It's not that avoiding them isn't the primary motivation for formalization because they don't happen. It's not the primary motivation because mistakes in math papers happening sometimes is OK. If some result is wrong (as opposed to just details in a proof which could be fixed) and it turns out to be an important result, the mistake is found eventually. This fairly rare occurrence wastes some time for people who maybe used the result and build upon it, but arguably a lot less time than it would take to formalize all papers with existing tools. This might change in the coming decades as formalization becomes easier. The perspective that this is not the main motivation is also the position of people working on Lean's Mathlib. E.g. Kevin Buzzard has said this at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Array.2EanyM.20is.20inconsistent/near/396178821 https://leanprover.zulipchat.com/#narrow/stream/270676-lean4...
  - 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)

trevyn 3y ago

>most formalizing effort is not primarily motivated by a desire to make sure there are no errors in the math. Is this because the proof author is generally confident that the proof is essentially correct?

staunton 3y ago
Here's people who are working on Lean's Mathlib discussing this https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Array.2EanyM.20is.20inconsistent/near/396178821 https://leanprover.zulipchat.com/#narrow/stream/270676-lean4...

t_mann 3y ago

Mathematicians might not like the insinuation, but the best reason to formalize mathematics is indeed to check its correctness: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_buzzard.pdf https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/sli... tl;dr: contradictory stuff even gets published in the likes of Annals of Mathematics, and even top journals are reluctant to retract published proofs that have later been shown to be false (which in itself shouldn't be possible). Like it or not, the reasons for formalizing mathematics abound, and they have a lot to do with the fact that humans are fallible, but mathematics shouldn't be. The incredibly tedious work of tracking down a proof's correctness to the last axiom is, while overwhelming for humans, exactly the kind of work that classical computers excel at.

staunton 3y ago
Of course there's mistakes in papers. It's not that avoiding them isn't the primary motivation for formalization because they don't happen. It's not the primary motivation because mistakes in math papers happening sometimes is OK. If some result is wrong (as opposed to just details in a proof which could be fixed) and it turns out to be an important result, the mistake is found eventually. This fairly rare occurrence wastes some time for people who maybe used the result and build upon it, but arguably a lot less time than it would take to formalize all papers with existing tools. This might change in the coming decades as formalization becomes easier. The perspective that this is not the main motivation is also the position of people working on Lean's Mathlib. E.g. Kevin Buzzard has said this at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Array.2EanyM.20is.20inconsistent/near/396178821 https://leanprover.zulipchat.com/#narrow/stream/270676-lean4...
- 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)