4 ms·
> 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?
by bumbledraven 2y ago
> 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?
- Tainnor 2y agoFor 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.
- optimalsolver 2y ago>of all possible theorems almost none have short proofs Ok, but what about the theorems humans would actually care about?
- Tainnor 2y agoWe 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).