Hacker News Reader

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