On: Did Turing prove the undecidability of the halting...

[FartyMcFarter]

What do you mean by dressing it up as a theorem? It is a theorem because there's a proof for it.

[Tainnor → FartyMcFarter]

For example, here's a formally verified proof in Lean: https://github.com/leanprover-community/mathlib4/blob/124731...