4 ms·
http://news.ycombinator.com/item?id=760547 http://news.ycombinator.com/item?id=760547 There was some discussion on the original post to HN about this announcem
by gdp 17y ago
http://news.ycombinator.com/item?id=760547 http://news.ycombinator.com/item?id=760547
There was some discussion on the original post to HN about this announcement. In particular, look at this:
http://ertos.nicta.com.au/research/l4.verified/proof.pml http://ertos.nicta.com.au/research/l4.verified/proof.pml
Which talks about the limits of provability.
In short, a "proof" that contains errors isn't really a proof of anything. And you build your proof inside an automated theorem prover so that it can be mechanically checked for internal inconsistency (i.e. contradictions), or for a completely inability to be false (i.e. tautologies).
- ilyak 17y agoYour automated theorem prover contains bugs, too.
- gdp 17y agoRead the link. If you understand a little bit about how something like Isabelle is constructed, only a small number of axioms are "hand coded", and then the rest is built from those. You can always build an external proof checking tool that checks that the proof you've constructed is correct. And if you're not confident in that, you can build another one.