3 ms·
So you say that the computer verified proofs of the incompleteness theorem of verifying the wrong theorem? Because there can't be bugs in a computer verified pr
by deadbeef57 5y ago
So you say that the computer verified proofs of the incompleteness theorem of verifying the wrong theorem? Because there can't be bugs in a computer verified proof.
(Of course there can theoretically be bugs in a computer verified proof. If there are bugs in the verifier. But if 4 independent proof assistants verify a proof of a theorem, this is extremely unlikely.)
- ProfHewitt 5y agoA proof is only as good as definitions and axioms used in the proof. All of the computer-verified proofs of existence of [Gödel 1931] proposition I'mUnprovable left out the order of proposition in its Gödel number :-(