3 ms·
This is addressed by the de Bruijn Criterion. The essential idea is that a small number of "trusted" rules should be enough to satisfy even the largest proofs.
by agentultra 2y ago
This is addressed by the de Bruijn Criterion. The essential idea is that a small number of "trusted" rules should be enough to satisfy even the largest proofs. You have to keep the number of rules small enough that they can be reviewed and understood by humans so that you can trust the proofs verified by the kernel.
- n4r9 2y agoThat probably helps to reduce the occurrence of issues, but I feel you are still ultimately relying on the correctness of proof assistants like Coq. And I am sure that bugs are occasionally found in Coq!
- agentultra 2y agoIndeed it does happen and it's unavoidable. You have to pick your axioms from somewhere and sometimes we pick the wrong ones or we find errors in our definitions. There's no "complete" or "perfect" system.