News for hackers. Stuff that matters.
Re:How close are computers to automating mathematical reason... by steve_musk on Saturday August 29, 2020 @12:31PM (#24317263)
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.

Re:How close are computers to automating mathematical reason... by qayxc on Saturday August 29, 2020 @12:43PM (#24317363)
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...

Re:How close are computers to automating mathematical reason... by tsimionescu on Saturday August 29, 2020 @12:52PM (#24317437)
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.
Re:How close are computers to automating mathematical reason... by pdehaan on Saturday August 29, 2020 @03:42PM (#24318869)
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"?

Re:How close are computers to automating mathematical reason... by roywiggins on Saturday August 29, 2020 @12:59PM (#24317503)
Which undecidable theorems have humans proven?
Re:How close are computers to automating mathematical reason... by dnautics on Saturday August 29, 2020 @01:19PM (#24317671)
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".