5 ms·

The usual maneuver by which mathematicians leverage that formal notion to capture the arguments they, and all their colleagues, regard as proofs is to say a pro

The usual maneuver by which mathematicians leverage that formal notion to capture the arguments they, and all their colleagues, regard as proofs is to say a proof is a finite sequence of assertions that could be filled in to become one of those formal structures. It’s not a bad approach if the goal is to give someone a general idea of what a proof is. The trouble is, no one has ever carried out that filling-in process. It’s purely hypothetical. False. What is "hypothetical" about this formal proof that the reals are uncountable? http://us.metamath.org/mpegif/ruc.html http://us.metamath.org/mpegif/ruc.html Each step is clickable, and just a few clicks take you back to the axioms. For more, see chapter 1 of the Metamath Book (http://us.metamath.org/downloads/metamath.pdf http://us.metamath.org/downloads/metamath.pdf) How is it that Devlin is unaware of logical systems like Metamath? It's at least 10 years old. [Edit: Maybe 20 years? 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."]

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
- _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.
CHY872 12y ago
Well, the author's point is probably still generally correct - in almost all fields proofs are not presented from axioms, and you could easily go your whole life as a mathematician without encountering such a proof, except perhaps by accident. The example you gave is the sort of proof presented to bright high school students - I'm sure you can do more interesting things with metamath, but I feel confident in saying that if you're a research mathematician, you'll lose a lot of time learning it and using it. Where proof assistants are used, they're frequently totally counter to the style of thinking traditionally taught in mathematics and computer science - I've heard them described by experts in the field as 'proof obstructions'. I'm currently writing my undergraduate project in a proof assistant, and you end up with tonnes of unreadable garbage like ASM_SIMP_TAC (srw_ss ()) [DETERMINACY_LEMMA, simp_expand_def] THEN1 METIS_TAC [] THEN RW_TAC (srw_ss ()) [ss_ecases] THEN FULL_SIMP_TAC (srw_ss ()) []. which has no real relation to any normal thought. Proving the determinacy of a relation took a matter of days of careful thinking (as a newbie to the package) - despite being able to prove it in a couple of lines of handwritten prose. I can imagine that this would be a massive turn-off for almost any research student. I also think that his line (it almost certainly is not, but more pertinent, how could you ever be sure it is?) is still a good point - you're trusting your correctness to a computer program, and all of the libraries built on top of it. The chances that one of these has a bug in (by this I mean a bug in the rules of inference of the theory) that could lead to the theory outputting garbage is probably quite high.
- madez 12y ago
  > I'm sure you can do more interesting things with metamath, but I feel confident in saying that if you're a research mathematician, you'll lose a lot of time learning it and using it. And then save time because you can be sure that the proofs you write are correct. > I'm currently writing my undergraduate project in a proof assistant, and you end up with tonnes of unreadable garbage like ASM_SIMP_TAC (srw_ss ()) [DETERMINACY_LEMMA, simp_expand_def] THEN1 METIS_TAC [] THEN RW_TAC (srw_ss ()) [ss_ecases] THEN FULL_SIMP_TAC (srw_ss ()) []. > which has no real relation to any normal thought. Proving the determinacy of a relation took a matter of days of careful thinking (as a newbie to the package) - despite being able to prove it in a couple of lines of handwritten prose. Did you try isar? > I also think that his line > (it almost certainly is not, but more pertinent, how could you ever be sure it is?) > is still a good point - you're trusting your correctness to a computer program, and all of the libraries built on top of it. The chances that one of these has a bug in (by this I mean a bug in the rules of inference of the theory) that could lead to the theory outputting garbage is probably quite high. It's not at all a good point. There are theorem provers that rely on the correctness of just a very small kernel. Everything on top (libraries) is then guaranteed to follow the rules imposed by the kernel.
placebo 12y ago
Interesting. I've thought about this exact topic before and I think his point shouldn't be dismissed so lightly. What got me thinking about this was an occasion (years ago) when I read a proof in which I didn't understand the jump from one assertion to the next one. It occurred to me then that the atomicity in these proofs (on which the entire structure stands) boils down to steps which are considered to be obvious. However "obvious" is a relative term, not an absolute one. So, at least as most proofs are concerned (and most proofs are not machine generated), his point is valid. As for systems like Metamath - how rigorous are the proofs that the software is bug free ? If you really want to philosophise over this, I'd even suggest that ultimately one can't really prove anything. At most, you can believe some assertion is correct to the degree you trust your senses, memory and logic - but I'll stop before this devolves into metaphysics...
- bumbledraven 12y ago
  As for systems like Metamath - how rigorous are the proofs that the software is bug free ? The formal system itself is transparently simple. You can easily verify the proofs by hand. Also the system has been reimplemented in several languages.
- sp332 12y ago
  Metamath gives 25,933 steps in proving that 2+2=4. http://us.metamath.org/mpegif/mmset.html#trivia http://us.metamath.org/mpegif/mmset.html#trivia

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

CHY872 12y ago

Well, the author's point is probably still generally correct - in almost all fields proofs are not presented from axioms, and you could easily go your whole life as a mathematician without encountering such a proof, except perhaps by accident. The example you gave is the sort of proof presented to bright high school students - I'm sure you can do more interesting things with metamath, but I feel confident in saying that if you're a research mathematician, you'll lose a lot of time learning it and using it. Where proof assistants are used, they're frequently totally counter to the style of thinking traditionally taught in mathematics and computer science - I've heard them described by experts in the field as 'proof obstructions'. I'm currently writing my undergraduate project in a proof assistant, and you end up with tonnes of unreadable garbage like ASM_SIMP_TAC (srw_ss ()) [DETERMINACY_LEMMA, simp_expand_def] THEN1 METIS_TAC [] THEN RW_TAC (srw_ss ()) [ss_ecases] THEN FULL_SIMP_TAC (srw_ss ()) []. which has no real relation to any normal thought. Proving the determinacy of a relation took a matter of days of careful thinking (as a newbie to the package) - despite being able to prove it in a couple of lines of handwritten prose. I can imagine that this would be a massive turn-off for almost any research student. I also think that his line (it almost certainly is not, but more pertinent, how could you ever be sure it is?) is still a good point - you're trusting your correctness to a computer program, and all of the libraries built on top of it. The chances that one of these has a bug in (by this I mean a bug in the rules of inference of the theory) that could lead to the theory outputting garbage is probably quite high.

madez 12y ago
> I'm sure you can do more interesting things with metamath, but I feel confident in saying that if you're a research mathematician, you'll lose a lot of time learning it and using it. And then save time because you can be sure that the proofs you write are correct. > I'm currently writing my undergraduate project in a proof assistant, and you end up with tonnes of unreadable garbage like ASM_SIMP_TAC (srw_ss ()) [DETERMINACY_LEMMA, simp_expand_def] THEN1 METIS_TAC [] THEN RW_TAC (srw_ss ()) [ss_ecases] THEN FULL_SIMP_TAC (srw_ss ()) []. > which has no real relation to any normal thought. Proving the determinacy of a relation took a matter of days of careful thinking (as a newbie to the package) - despite being able to prove it in a couple of lines of handwritten prose. Did you try isar? > I also think that his line > (it almost certainly is not, but more pertinent, how could you ever be sure it is?) > is still a good point - you're trusting your correctness to a computer program, and all of the libraries built on top of it. The chances that one of these has a bug in (by this I mean a bug in the rules of inference of the theory) that could lead to the theory outputting garbage is probably quite high. It's not at all a good point. There are theorem provers that rely on the correctness of just a very small kernel. Everything on top (libraries) is then guaranteed to follow the rules imposed by the kernel.

placebo 12y ago

Interesting. I've thought about this exact topic before and I think his point shouldn't be dismissed so lightly. What got me thinking about this was an occasion (years ago) when I read a proof in which I didn't understand the jump from one assertion to the next one. It occurred to me then that the atomicity in these proofs (on which the entire structure stands) boils down to steps which are considered to be obvious. However "obvious" is a relative term, not an absolute one. So, at least as most proofs are concerned (and most proofs are not machine generated), his point is valid. As for systems like Metamath - how rigorous are the proofs that the software is bug free ? If you really want to philosophise over this, I'd even suggest that ultimately one can't really prove anything. At most, you can believe some assertion is correct to the degree you trust your senses, memory and logic - but I'll stop before this devolves into metaphysics...

bumbledraven 12y ago
As for systems like Metamath - how rigorous are the proofs that the software is bug free ? The formal system itself is transparently simple. You can easily verify the proofs by hand. Also the system has been reimplemented in several languages.
sp332 12y ago
Metamath gives 25,933 steps in proving that 2+2=4. http://us.metamath.org/mpegif/mmset.html#trivia http://us.metamath.org/mpegif/mmset.html#trivia