Hacker News Reader

Comment by Confusion | Hacker News Reader

If formally precise reasoning would be all there is to it, computers could do all math for us. However, even in that formal-if-anyhing-is area, they fail. Computers can't solve instances of the Halting problem or the Tiling problem, whose solution is immediately intuitively clear to a human. Those solution can also be immediately verified by fellow humans, via the informal communication method of 'speech'. The reasoning involved can't be verified by computers.

A nice overview was given by Peter of Conscious Entities recently: http://www.consciousentities.com/?p=1918.

View on HN

Actually computers can solve many instances of the halting problem. http://en.wikipedia.org/wiki/Microsoft_Terminator

Yes. The point is there are many instances that humans can solve, but computers can't. My sentence was not meant to imply computers cannot solve any instances of the halting problem at all.

> Computers can't solve instances of the Halting problem or the Tiling problem, whose solution is immediately intuitively clear to a human.

This is unclear. Do you mean that computers can't solve the Halting Problem, but humans can solve many instances of the question "will this question halt"? Then you're not comparing apples with apples. You should instead compare human reasoning of "this program will halt or not" with programs developed in the field of termination analysis. Are these analysis bad compared to human ones?

Or do you mean that humans can prove the undecidability of the Halting Problem, but computers can't manage to prove or disprove it, or understand the human proofs? Does this have to do with such proofs tend to be non-constructive, as far as I've seen?

In any case, I guess it's still an open problem whether or not the human mind can algorithmically solve the Halting Problem, right? Our minds would have to be "better" than a TM.

Yes, the latter is exactly the open question. It's one that has had us stumped for decades and on which barely any progress has been made. There are simple examples of purely mathematical problems that we can't seem to teach computers how to solve, even though they are trivial for humans. Of course it's entirely possible we will find a way to teach machines how to solve them. It would be even more interesting if some AI developed the ability to solve them and could subsequently explain how it does it.

> Those solution[s] can also be immediately verified by fellow humans, via the informal communication method of 'speech'. The reasoning involved can't be verified by computers.

This isn't a particularly strong argument, as solutions verified via the informal communication method of 'speech' often pass verification without being correct.

Yes, humans are capable of doing math incorrectly. That is irrelevant to an argument explaining that computers are incapable of doing some math at all.

Reply on news.ycombinator.com