3 ms·
Read 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 re
by gdp 17y ago
Read 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.