[steve_musk]

A human is no more capable of solving the halting problem than a computer.

And we aren’t doing some kind of magical logic when we humans create proofs. Sure naively general automated proof generation could be exponential in nature, but that hasn’t stopped us from mathematics research. There’s no reason it should stop computers either.

[qayxc]

But we are (in general).

Humans can solve problems that aren't solvable by algorithms and that's why humans can - in general - decide whether a given program will halt. That doesn't mean every human can or that it has been done for every program (which would be impossible, since there are infinitely many instances anyway).

But the difference between humans and Turing Machines (computers) is, that humans can and did proof undecidable problems, while algorithms provably can't.

This is a fundamental difference and there's no way around it. So whatever might be done in ATP, it can't be algorithmic in nature or based on a Turing Machine in order to be applied universally.

Unless of course, you know of a way to disprove Gödel and Turing...

[tsimionescu]

I don't know what made you believe this, but humans are not magical. We absolutely can't solve the halting problem, and by definition nothing can decide an undecidable problem. As far as we know so far, the human mind is a (limited) Turing machine. In fact, as far as we know, there is no computing system more powerful than a Turing machine.

[pdehaan]

Are there any problems we have a proof for, and a corresponding proof that no algorithm can exist to provide said proof?

Basically, why can't I write an algorithm that can be given input for "is the halting problem decidable?" and return "no"?

[roywiggins]

Which undecidable theorems have humans proven?

[dnautics]

yeah that's not a thing. Humans do regularly "solve" undecidable theorems, if by solve you mean "come up with heuristics that are good enough". Possibly even "provably good enough", as in "if there's a flaw in the algorithm, the lower bound on the badness of the input to make it unreachable in the lifetime of the universe".