Lovely poem. One reading of it is something like "if computers can't prove that computer proofs are always correct, then we can't be sure of anything", but tha

Lovely poem. One reading of it is something like "if computers can't prove that computer proofs are always correct, then we can't be sure of anything", but that is true of human proofs as well, so we might as well Ctrl-W mathematics itself. Another reading is something like "this very introductory article didn't mention whether we can formalize Gödel's incompleteness results in the computer, so it's too introductory for me". Fair enough.