Behind this ridiculous silliness is a serious point: proof is a rhetorical device, not a mechanical process; the purpose of proof is to •convince•. Language is slippery. Thought is slippery. There is always a gap between (language + assumptions + human thought) and Platonic mathematical abstraction. Attempts to mechanize proof do not actually close this gap; they just move some things to the other side of it. You can’t escape that gap — and that gap is the •heart• of mathematics.
3/