Hacker News Reader

I know of several computer verified proofs of the incompleteness theorem. See entry 6 of https://www.cs.ru.nl/~freek/100/ for a small catalogue. How does this relate to your objection? Are there bugs in the verifiers? Or did people verify the wrong theorem statement?

View on HN

Proofs forgot to include order of proposition in its Gödel number.

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.)

A 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 :-(

Reply on news.ycombinator.com