2 ms·
Your automated theorem prover contains bugs, too.
by ilyak 17y ago
Your 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.