What makes those proofs any different from proofs of other mathematical theorems? I imagine that the halting problem, in particular, would not be beyond the capability of some existing automated theorem prover, assuming you could encode the statement; its proof isn’t too involved.
If your argument is that humans understand these proofs because of some magical out-of-the-box-thinking ability, then I am skeptical.
What makes those proofs any different from proofs of other mathematical theorems? I imagine that the halting problem, in particular, would not be beyond the capability of some existing automated theorem prover, assuming you could encode the statement; its proof isn’t too involved.
If your argument is that humans understand these proofs because of some magical out-of-the-box-thinking ability, then I am skeptical.