What is a proof, really?
profkeithdevlin.org
profkeithdevlin.org
False. What is "hypothetical" about this formal proof that the reals are uncountable? 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)
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 says "The name "Metamath" has been used publicly by Norman Megill since 1994 to refer to a computer language and related software."]
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.
https://www.maa.org/external_archive/devlin/devlin_01_05.htm...
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.
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_Foundation...)
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.
(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. :)
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).
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.
There are certainly some stodgy holdouts that will never be convinced, but I don't think Devlin is one of them.
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.
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.
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.
For better or worse, we both know that's not required to be a successful mathematician. I remember reading a presentation from a guy advocating mechanised proof who realised that almost every important proof in his field had been later shown to be false.
> Did you try isar?
I had a go at using Isabelle (in general) and truthfully never really got onto Isar - I discovered that both my supervisors have written large theories in HOL4 (JIT compilers etc), but have no recent experience with Isabelle, so that's what I'm using. I've seen examples of Isar which look nice, but I'm skeptical about its scalability. You make a good point, thouugh.
> 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.
Yes, of course - but the richness of a theorem prover comes from the logics you define on top of it.
If the library implementation of a particularly complex structure defined externally to the logic with no easy to coverify definition had a mistake in its definition which is not caught, any entailed inconsistencies are transmitted to the theorems that rely on this data structure.
Sure, your theorems are correct in the logic - but they might not be useful. I obviously pick the more engineering based example, but that's merely due to my being ignorant of most pure mathematics - there are probably analogues.
This is a growing problem for companies like Intel, who use a software model to test their firmwares before the hardware is available [1] - they want to verify that the operations are identical.
[1] - http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/papers/44-...
Some professors I know told me something along those lines about various topics of mathematics. The more advanced the topic gets the less people cope with the complexity. In the end it gets so specialized that only a few people in the world can and are willing to follow the advance. That situation combined with human notorious fallibility brings mathematic research in a very bad situation.
I makes me sad - and angry I have to admit - that the professors I met don't recognize computer-aid as the solution. Besides that I personally had the most pleasure doing mathematics while being guarded by a computer against my stupidity[+].
> Yes, of course - but the richness of a theorem prover comes from the logics you define on top of it.
> If the library implementation of a particularly complex structure defined externally to the logic with no easy to coverify definition had a mistake in its definition which is not caught, any entailed inconsistencies are transmitted to the theorems that rely on this data structure.
> Sure, your theorems are correct in the logic - but they might not be useful. I obviously pick the more engineering based
[+] You raise a good point. The computer can't do all the work. Nevertheless it's a huge advance to only have to verify the definitions and theorem statements instead of all that combined with the proofs. It's like having to remember the summary of a book instead of the whole book. Someday we will hit a wall even when using computers but that shouldn't stop us know.
> This is a growing problem for companies like Intel, who use a software model to test their firmwares before the hardware is available [1] - they want to verify that the operations are identical.
Thats awesome! Nice problem to work on. Stories like this keep my dream alive that there are interesting workplaces in this world.
His point was that formal proofs are "hypothetical", not that they are rarely encountered. What part of
> The trouble is, no one has ever carried out that filling-in process. It’s purely hypothetical.
don't you understand?
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.
The syntax you describe bears very little relation to formal system like Metamath in which proofs are readily checkable by people and machines.
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.
No. Metamath proofs can easily be verified by hand.
Addendum: the above is mostly tangential to the original article. The author is very correct that a modern mathematical proof exists, and is formulated to, show another person with suitable background how to work out the truth of a statement. But don't let this form of proof distract you from the existence of the foundations of rigorous proof in general; just as we don't let Ruby's English-like syntax convince us that we aren't truly executing computation. The foundations of mathematical logic are complex, like the transistors on a microchip, but they do "work," in the strongest epistemological sense of the word.
I find that difficult to believe. My basic math courses in college taught proofs using axioms, starting with really basic stuff like proving that the product of two even integers is an even integer. I don't see how anyone with a mathematics degree could miss that, or could do much useful work without that.
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...
The formal system itself is transparently simple. You can easily verify the proofs by hand. Also the system has been reimplemented in several languages.
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.
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.
> 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.
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.
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.
As they say, that is, until you do machine learning.