5 ms·

You are right in stating that what he is saying is false. There are a lot of proofs written with assistance of Coq or Isabelle/HOL that can easily be extended

by madez 12y ago

You are right in stating that what he is saying is false. There are a lot of proofs written with assistance of Coq or Isabelle/HOL that can easily be extended to include each and every logical step. That he said what he said saddens me a lot. Machine-checked mathematical proofs are the future of mathematics and most mathematicians I know are totally ignorant about them.

gre 12y ago
He's clearly not ignorant of computer assisted proofs, but I also wish he'd show more enthusiasm for them. https://www.maa.org/external_archive/devlin/devlin_01_05.html https://www.maa.org/external_archive/devlin/devlin_01_05.htm...
- deleted 12y ago
  [deleted]
- dvanduzer 12y ago
  Given the software engineering tools available in 1976 (and again in 1994), can you offer a defensible reason he should've been more enthusiastic?
  - bumbledraven 12y ago
    I think Metamath was available in 1994. (http://us.metamath.org/copyright.html http://us.metamath.org/copyright.html says: The name "Metamath" has been used publicly by Norman Megill since 1994 to refer to a computer language and related software.) And even if Devlin wasn't aware of it (or systems like it) back then, what's his excuse now?
  - gre 12y ago
    What does 1994 have to do with it? Homotopy type theory as a framework for doing proofs is exciting. Vladimir Voevodsky had a talk somewhere on youtube in which he claimed you could get similar length proofs in Coq using HoTT as you could on paper. He's also excited about the prospect of most math papers publishing machine-checked proofs. I wish I could find the exact video for you.
    - nova 12y ago
      > He's also excited about the prospect of most math papers publishing machine-checked proofs. Apparently the feels he can't be sure of the correctness of his own papers without machine checked proofs anymore, and he's a Fields medal winner: I now do my mathematics with a proof assistant and do not have to worry all the time about mistakes in my arguments or about how to convince others that my arguments are correct. But I think that the sense of urgency that pushed me to hurry with the program remains. Sooner or later computer proof assistants will become the norm, but the longer this process takes the more misery associated with mistakes and with unnecessary self-verification the practitioners of the field will have to endure (from this http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundation...)
      - dvanduzer 12y ago
        Vladimir Voevodsky may feel that way, but we were talking about Keith Devlin. To answer gre's question, 1994 is the year Devlin cites a major breakthrough in the four color problem, in the very link that gre cited as an example of Devlin's lack of enthusiasm about machine checked proofs. There are plenty of good reasons to mistrust machines when it comes to mathematical proofs, and mathematicians have been correct in their skepticism. Most of the work in Univalent Foundations has been directly aimed at addressing that skepticism. Optimism from its proponents in the 2010s is just as valid as the skepticism in the 70s and 90s. And I mean just as valid in a very specific way; specifically in the spirit of the originally linked Devlin post published today.
    - dvanduzer 12y ago
      I'm excited about HoTT, too. If anyone has demonstrated a short proof of the four-color map theorem in Coq, that would meet Devlin's criteria for convincing machine-checked proofs. (Check the link you cited; Devlin mentions 1976 and 1994 as key milestones for machine-checked proofs) But HoTT and Coq are both still new, particularly when speaking of mathematics. When they figure out how to make LaTeX produce their textbook in a fully MathML-compatible fashion, then we can talk. :)
_asummers 12y ago
This is a good talk to show to those mathematicians. Machine checked proofs are way too powerful to ignore. https://www.youtube.com/watch?v=zmhd8clDd_Y https://www.youtube.com/watch?v=zmhd8clDd_Y
- dvanduzer 12y ago
  As your cousin post notes, Devlin isn't ignoring "machine checked" proofs. The question of whether machines can write proofs that can be "human checked" is the far more interesting question to a mathematician. Otherwise, they'd be software engineers (which Devlin hints at in this essay).
  - bumbledraven 12y ago
    The question of whether machines can write proofs that can be "human checked" is the far more interesting question to a mathematician. Maybe Devlin should first stop denying that humans can write proofs that can be both human- and machine- checked. Then we can talk about whether machines can write those proofs.
    - dvanduzer 12y ago
      Humans can definitely write proofs that can be checked by humans or machines. It's arguing in bad faith to suggest that mathematicians are un-qualified to determine the validity of a machine-checked proof. There are certainly some stodgy holdouts that will never be convinced, but I don't think Devlin is one of them.
  - _asummers 12y ago
    I wasn't suggesting that Devlin was ignoring them, I was responding to my comment's parent that mathematicians he knows are ignorant of them, which I tried to make clear by saying "those mathematicians".
ninguem2 12y ago
>Machine-checked mathematical proofs are the future of mathematics I don't disagree. >most mathematicians I know are totally ignorant about them Most of them realize that this is a possibility but believe, rightly or wrongly, that they are not going to be relevant in their lifetime.

by madez 12y ago

gre 12y ago

He's clearly not ignorant of computer assisted proofs, but I also wish he'd show more enthusiasm for them. https://www.maa.org/external_archive/devlin/devlin_01_05.html https://www.maa.org/external_archive/devlin/devlin_01_05.htm...

deleted 12y ago
[deleted]
dvanduzer 12y ago
Given the software engineering tools available in 1976 (and again in 1994), can you offer a defensible reason he should've been more enthusiastic?
- bumbledraven 12y ago
  I think Metamath was available in 1994. (http://us.metamath.org/copyright.html http://us.metamath.org/copyright.html says: The name "Metamath" has been used publicly by Norman Megill since 1994 to refer to a computer language and related software.) And even if Devlin wasn't aware of it (or systems like it) back then, what's his excuse now?
- gre 12y ago
  What does 1994 have to do with it? Homotopy type theory as a framework for doing proofs is exciting. Vladimir Voevodsky had a talk somewhere on youtube in which he claimed you could get similar length proofs in Coq using HoTT as you could on paper. He's also excited about the prospect of most math papers publishing machine-checked proofs. I wish I could find the exact video for you.
  - nova 12y ago
    > He's also excited about the prospect of most math papers publishing machine-checked proofs. Apparently the feels he can't be sure of the correctness of his own papers without machine checked proofs anymore, and he's a Fields medal winner: I now do my mathematics with a proof assistant and do not have to worry all the time about mistakes in my arguments or about how to convince others that my arguments are correct. But I think that the sense of urgency that pushed me to hurry with the program remains. Sooner or later computer proof assistants will become the norm, but the longer this process takes the more misery associated with mistakes and with unnecessary self-verification the practitioners of the field will have to endure (from this http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundation...)
    - dvanduzer 12y ago
      Vladimir Voevodsky may feel that way, but we were talking about Keith Devlin. To answer gre's question, 1994 is the year Devlin cites a major breakthrough in the four color problem, in the very link that gre cited as an example of Devlin's lack of enthusiasm about machine checked proofs. There are plenty of good reasons to mistrust machines when it comes to mathematical proofs, and mathematicians have been correct in their skepticism. Most of the work in Univalent Foundations has been directly aimed at addressing that skepticism. Optimism from its proponents in the 2010s is just as valid as the skepticism in the 70s and 90s. And I mean just as valid in a very specific way; specifically in the spirit of the originally linked Devlin post published today.
  - dvanduzer 12y ago
    I'm excited about HoTT, too. If anyone has demonstrated a short proof of the four-color map theorem in Coq, that would meet Devlin's criteria for convincing machine-checked proofs. (Check the link you cited; Devlin mentions 1976 and 1994 as key milestones for machine-checked proofs) But HoTT and Coq are both still new, particularly when speaking of mathematics. When they figure out how to make LaTeX produce their textbook in a fully MathML-compatible fashion, then we can talk. :)

_asummers 12y ago

This is a good talk to show to those mathematicians. Machine checked proofs are way too powerful to ignore. https://www.youtube.com/watch?v=zmhd8clDd_Y https://www.youtube.com/watch?v=zmhd8clDd_Y

dvanduzer 12y ago
As your cousin post notes, Devlin isn't ignoring "machine checked" proofs. The question of whether machines can write proofs that can be "human checked" is the far more interesting question to a mathematician. Otherwise, they'd be software engineers (which Devlin hints at in this essay).
- bumbledraven 12y ago
  The question of whether machines can write proofs that can be "human checked" is the far more interesting question to a mathematician. Maybe Devlin should first stop denying that humans can write proofs that can be both human- and machine- checked. Then we can talk about whether machines can write those proofs.
  - dvanduzer 12y ago
    Humans can definitely write proofs that can be checked by humans or machines. It's arguing in bad faith to suggest that mathematicians are un-qualified to determine the validity of a machine-checked proof. There are certainly some stodgy holdouts that will never be convinced, but I don't think Devlin is one of them.
- _asummers 12y ago
  I wasn't suggesting that Devlin was ignoring them, I was responding to my comment's parent that mathematicians he knows are ignorant of them, which I tried to make clear by saying "those mathematicians".

ninguem2 12y ago

>Machine-checked mathematical proofs are the future of mathematics I don't disagree. >most mathematicians I know are totally ignorant about them Most of them realize that this is a possibility but believe, rightly or wrongly, that they are not going to be relevant in their lifetime.