6 ms·

What is a proof, really?

62 points by CarolineW 12y ago

bumbledraven 12y ago
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...)
  - _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
bitwarrior 12y ago
"What kind of a proof? It's a proof. A proof is a proof. And when you have a good proof, it's because it's proven." - Jean Chretien https://www.youtube.com/watch?v=aX6XMIldkRU https://www.youtube.com/watch?v=aX6XMIldkRU
debacle 12y ago
It seems like the author is conflating the accuracy of the language of a proof with the accuracy of the proof itself, which may be the same thing to some extent, but overall to try and refute something like this: > In particular, they believe proofs are fundamentally and exclusively about truth, and that they are either right or wrong. ...is just semantics. Arguing that a Euclidean proof is wrong because it makes contextual assumptions about the reader's frame of reference is just pedantry. Mathematics is much more rigorous in 2014 because the value of the time of the average mathematician is worth much less.
hyp0 12y ago
Professional mathematics is more like English Literature than computer programming: you need extensive background in the area to follow it; and you can't just run it to see if it works.
- madez 12y ago
  I don't agree. Did you ever try Isabelle/HOL? It let's you "run it" to see if it works.
  - anonymousDan 12y ago
    How many professional mathematicians use Isabelle/HOL? Honest question!
    - yummyfajitas 12y ago
      Close to none. Part of that is a social problem. People who do computer assisted proofs are not particularly well regarded, in my experience. Another big issue with those tools is that they don't work as well for analysis as they do for algebraic geometry and graph theory. This might be in part due to the fact that most of the folks constructing them are logicians, not analysts.
mjklin 12y ago
> with a once comforting illusion of crisp, clean certainty rapidly giving way to a panicked feeling of sinking into shifting quicksand. Sounds like he is describing the intellectual development of Bertrand Russell, who spent ten years proving that 1+1=2. Legend has it that his huge book on the subject (Principia Mathematica) has never been read cover to cover. With such precedents as Russell and Wittgenstein it's ridiculous for any modern person to expect "crisp, clean certainty" in anything involving language.
- yummyfajitas 12y ago
  He didn't spend 10 years proving 1+1=2. He spent 10 years constructing an axiomatic system in which arithmetic and everything else could be proved.
  - mjklin 12y ago
    Which then got the rug pulled out from under by Gödel
wyager 12y ago
Absolutely false. We have a large number of machine-checked proof that are 100% "filled in". As a trivial example that a fair number of CS people might have been exposed to: every time someone compiles an Agda program, the compiler does a complete formal proof that the program is total and terminating.
mattxxx 12y ago
This is a pretty sensational piece, but there's fundamental truth in that what-a-proof-is is based on an individual's ability to understand it. This is just how all ideas work. In the end, you can then take a proof and make it empirical easily, and this (while not being anything like a proof) can be more convincing, because it's not tested by your understanding, but rather by your ability to observe... this also is fundamental to proof-by-contradiction, which convinces you simply by showing an example of a situation that doesn't work (and those disproves the assumption). I think there's a lot of criticism floating around here, but there's something fundamentally right about a proof being about communication. The truth the proof reveals is pretty much objective though.
avmich 12y ago
You think you know when you learn, are more sure when you can write, even more when you can teach, but certain when you can program. -- Alan Perlis As they say, that is, until you do machine learning.

62 points by CarolineW 12y ago

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

bitwarrior 12y ago

"What kind of a proof? It's a proof. A proof is a proof. And when you have a good proof, it's because it's proven." - Jean Chretien https://www.youtube.com/watch?v=aX6XMIldkRU https://www.youtube.com/watch?v=aX6XMIldkRU

debacle 12y ago

It seems like the author is conflating the accuracy of the language of a proof with the accuracy of the proof itself, which may be the same thing to some extent, but overall to try and refute something like this: > In particular, they believe proofs are fundamentally and exclusively about truth, and that they are either right or wrong. ...is just semantics. Arguing that a Euclidean proof is wrong because it makes contextual assumptions about the reader's frame of reference is just pedantry. Mathematics is much more rigorous in 2014 because the value of the time of the average mathematician is worth much less.

hyp0 12y ago

Professional mathematics is more like English Literature than computer programming: you need extensive background in the area to follow it; and you can't just run it to see if it works.

madez 12y ago
I don't agree. Did you ever try Isabelle/HOL? It let's you "run it" to see if it works.
- anonymousDan 12y ago
  How many professional mathematicians use Isabelle/HOL? Honest question!
  - yummyfajitas 12y ago
    Close to none. Part of that is a social problem. People who do computer assisted proofs are not particularly well regarded, in my experience. Another big issue with those tools is that they don't work as well for analysis as they do for algebraic geometry and graph theory. This might be in part due to the fact that most of the folks constructing them are logicians, not analysts.

mjklin 12y ago

> with a once comforting illusion of crisp, clean certainty rapidly giving way to a panicked feeling of sinking into shifting quicksand. Sounds like he is describing the intellectual development of Bertrand Russell, who spent ten years proving that 1+1=2. Legend has it that his huge book on the subject (Principia Mathematica) has never been read cover to cover. With such precedents as Russell and Wittgenstein it's ridiculous for any modern person to expect "crisp, clean certainty" in anything involving language.

yummyfajitas 12y ago
He didn't spend 10 years proving 1+1=2. He spent 10 years constructing an axiomatic system in which arithmetic and everything else could be proved.
- mjklin 12y ago
  Which then got the rug pulled out from under by Gödel

wyager 12y ago

Absolutely false. We have a large number of machine-checked proof that are 100% "filled in". As a trivial example that a fair number of CS people might have been exposed to: every time someone compiles an Agda program, the compiler does a complete formal proof that the program is total and terminating.

mattxxx 12y ago

This is a pretty sensational piece, but there's fundamental truth in that what-a-proof-is is based on an individual's ability to understand it. This is just how all ideas work. In the end, you can then take a proof and make it empirical easily, and this (while not being anything like a proof) can be more convincing, because it's not tested by your understanding, but rather by your ability to observe... this also is fundamental to proof-by-contradiction, which convinces you simply by showing an example of a situation that doesn't work (and those disproves the assumption). I think there's a lot of criticism floating around here, but there's something fundamentally right about a proof being about communication. The truth the proof reveals is pretty much objective though.

avmich 12y ago

You think you know when you learn, are more sure when you can write, even more when you can teach, but certain when you can program. -- Alan Perlis As they say, that is, until you do machine learning.