It has been shown numerous times that there are limits to automated proof generation.
One such result was that certain problems are undecidable, which means that any automated approach would be prone to become "stuck" and never terminate.
Another results showed that the complexity of general automated proof generation is exponential in nature.
Both these results mean, that it's impossible to tell whether a computation just takes a very long time (say years) or whether the problem is indeed undecidable (in which case the program would never halt.)
A human on the hand, is very well capable of solving the Halting Problem and can discern whether a problem is undecidable [1].
This is of course a corner case, but it goes to show that there are indeed limits to automated theorem proving.
A human would therefore - in principle - always need to proof that a problem is decidable in the first place before passing it to an ATP.
Humans are not able to solve the halting problem. The halting problem isn't a question of if you can decide that some programs will not halt, but that you can decide if all programs would halt.
No - that's simply not true. The Halting Problem states that there is no Turing Machine (i.e. program) capable of deciding whether a given program will halt.
And yes, humans are very well capable of solving that, because humans can in fact proof whether any program halts.
This doesn't mean every human can or that it has been done for every program, but it means that humans are - in general - able capable of deciding this, while algorithms
(programs) can't.
The Church-Turing thesis claims (and is believed to be right) that a Turing machine can solve (compute) any problem that can be solved (is computable).
For now at least, we don't know of any counter-example to the Church-Turing thesis. Humans are certainly not able to tell whether a program in general will halt for any input it recieves. If you believe otherwise, please tell me whether the following program halts:
Solving the halting problem means being able to tell, for ANY Turing machine and ANY input, whether it will halt. I know of absolutely nothing that would make us believe humanity or any individual human can do this.
If there is a single Turing machine for which there is no human that can tell whether it will halt, the conjecture that human reasoning is not more powerful than Turing machines is still not disproven.
Also, if you were right that humans can do things that Turing machines can't, it would be an interesting excersise to try to find that example of super-Turing human reasoning and try to see why it can't be encoded as a Turing machine. No one has successfully done this yet, so there is no reason to believe that it is possible.
There is no reason to believe that the human mind can solve a superset of the problems solvable by a Turing machine, and a lot of evidence to the contrary.
Also, the link you replied provides an argument of efficiency, not an argument of possibility. It is arguing that we might use things that are not Turing machines because they can solve the problem more efficiently, not because they can solve problems Turing machines could never hope to solve.
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.
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...
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.
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".
One such result was that certain problems are undecidable, which means that any automated approach would be prone to become "stuck" and never terminate.
Another results showed that the complexity of general automated proof generation is exponential in nature.
Both these results mean, that it's impossible to tell whether a computation just takes a very long time (say years) or whether the problem is indeed undecidable (in which case the program would never halt.)
A human on the hand, is very well capable of solving the Halting Problem and can discern whether a problem is undecidable [1].
This is of course a corner case, but it goes to show that there are indeed limits to automated theorem proving.
A human would therefore - in principle - always need to proof that a problem is decidable in the first place before passing it to an ATP.
[1] https://en.wikipedia.org/wiki/List_of_undecidable_problems