Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

> as we’ll discuss, it’s a basic metamathematical fact that out of all possible theorems almost none have short proofs

Where in the article is this discussed?



For any possible definition of "short", there's only finitely many (and typically few) theorems that have a short proof, while there are infinitely many theorems (not all of them interesting).

More in detail: Proofs are nothing more than strings, and checking the validity of a proof can be done mechanically (and efficiently), so we can just enumerate all valid proofs up to length N and pick out its conclusion.


>of all possible theorems almost none have short proofs

Ok, but what about the theorems humans would actually care about?


We can't really formalise what theorems humans would care about, so I'm afraid this is hard to answer rigorously.

But there are some theorems many people care about and they don't have any known short proofs (e.g. Fermat's Last Theorem).




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

Search: