> 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?
Where in the article is this discussed?
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.
Ok, but what about the theorems humans would actually care about?
But there are some theorems many people care about and they don't have any known short proofs (e.g. Fermat's Last Theorem).