> At one extreme lies the systems of formal proofs that encode proofs and theorems in an almost unrecognisable language “known only to a bunch of monks that live on a mountain"
I haven't read too far but I think this refers to the "classic" perspective on proofs which described in "Social Processes and Proofs of Theorems and Programs" [1]. The idea being that proofs should be derivable from first principles even if they are not in practice. This is in contrast to the "probabilistic" perspective which supposes that proofs are only ever "likely" to be correct.
I do a fair amount of work in Coq now and I've done extensive (first order logic) hand written proofs for the same material. So I guess I fall in to the classicist camp. There are a few things I like about this approach as I've experienced it:
Obviously there is no doubt about whether I've proven something. Or at worst there is an absolute minimum of doubt (down to the trusted computing base of Coq and CoC).
With a proof assistant I can easily play with my proof environment and try things out in the same way I do when I'm programming. I suppose this might also be true for more informal proofs but Proof General [2] makes it easy and enjoyable.
Most importantly, I can provide my encodings and proofs as a "library" that others can consume. At first glance this seems to have nothing to do with a classical view of proofs if they exist on paper, but I find higher level proof descriptions in papers hard to consume. Even when the proofs are in my area of expertise. Reading the mathematics fully laid out can be tedious but it contains all the answers to any questions you might have which can't always be said of more informal proofs.
To be fair, my area of expertise (PL) has extensive existing work in Coq and the tool works really well with these kinds of large but "shallow" proofs.
“Formal proof” and “mechanized proof” are not synonymous. And proof assistants have a long way to go before they can be useful for mathematics in general.
Proof of phi means you've informally convinced me that for all {<-}-structures A, if ZF or ZFC is true in A, then phi is true. This of course is different depending on whether you take ZF or ZFC as the axioms.
The idea that I'm going to write down what it means to convince me of this is equivalent to asking me to give up my authority to judge mathematical theorems. I'm not doing that. Computers can smell my farts as far as I'm concerned. And if a politician asks me to tell his computer what it will take for me to accept a proof, then he needs to slather his balls in marinade sauce, skewer them, and stick them in the broiler.
4 comments
[ 2.6 ms ] story [ 14.0 ms ] threadI haven't read too far but I think this refers to the "classic" perspective on proofs which described in "Social Processes and Proofs of Theorems and Programs" [1]. The idea being that proofs should be derivable from first principles even if they are not in practice. This is in contrast to the "probabilistic" perspective which supposes that proofs are only ever "likely" to be correct.
I do a fair amount of work in Coq now and I've done extensive (first order logic) hand written proofs for the same material. So I guess I fall in to the classicist camp. There are a few things I like about this approach as I've experienced it:
Obviously there is no doubt about whether I've proven something. Or at worst there is an absolute minimum of doubt (down to the trusted computing base of Coq and CoC).
With a proof assistant I can easily play with my proof environment and try things out in the same way I do when I'm programming. I suppose this might also be true for more informal proofs but Proof General [2] makes it easy and enjoyable.
Most importantly, I can provide my encodings and proofs as a "library" that others can consume. At first glance this seems to have nothing to do with a classical view of proofs if they exist on paper, but I find higher level proof descriptions in papers hard to consume. Even when the proofs are in my area of expertise. Reading the mathematics fully laid out can be tedious but it contains all the answers to any questions you might have which can't always be said of more informal proofs.
To be fair, my area of expertise (PL) has extensive existing work in Coq and the tool works really well with these kinds of large but "shallow" proofs.
1. https://d1b10bmlvqabco.cloudfront.net/attach/ixkltd3cjy12bv/...
2. https://proofgeneral.github.io
The idea that I'm going to write down what it means to convince me of this is equivalent to asking me to give up my authority to judge mathematical theorems. I'm not doing that. Computers can smell my farts as far as I'm concerned. And if a politician asks me to tell his computer what it will take for me to accept a proof, then he needs to slather his balls in marinade sauce, skewer them, and stick them in the broiler.
https://www.youtube.com/watch?v=53_000njVs4 Delicious testicle glaze