Hacker News new | past | comments | ask | show | jobs | submit login

> What I was trying to ask was if there are formally provable theories that cannot be expressed in a way that would let a computer "compute" the proof.

Do you mean "find the proof" or "verify the proof"? That difference is critical.

Theorem-provers that work to find proofs have made many strides, but as of today humans easily run rings around them. That's not to say it can never be done. Years ago good Go players could trounce machines, and that is no longer true. So: Today, most proofs cannot practically be found by a machine, but they are getting better and there's no fundamental reason computers can't be excellent at it.

Verifying proofs is something a computer is par excellence at. To verify a proof, the proof checker simply needs to verify that each step is valid. No human can compare to the ability of a computer to be picky :-).

In some systems it may not be possible to express a proof of a particular claim in a reasonably short sequence. But that would be a limitation for both humans and computers. In both cases, the answer would be the same: find a way to switch to a "different" system where it's easier to express the proof. In some sense normal math does this; people routinely define new terms, and then build on those definitions so that everything else is simpler.

I really hope machine learning will succeed in producing systems that surpass contemporary mathematicians in not only finding proofs, but also suggesting definitions and theorems to simplify a database of mathematics.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact