4 ms·
A smaller proof using fewer axioms or other proofs than the current state-of-the-art. Discovering new and "interesting" proofs. Don't ask me to define "intere
by ansible 9y ago
A smaller proof using fewer axioms or other proofs than the current state-of-the-art.
Discovering new and "interesting" proofs. Don't ask me to define "interesting" in this context.
- infinity0 9y agoIt's exactly my original point that these goals are not well-defined in early 21st century maths.
- seanwilson 9y agoIn the field of formal/machine proofs, nobody really cares about the length of the proofs because part of the point is the proofs are checked by the computer back to the basic axioms so you can trust the proofs are correct. Being able to discover long and ugly proofs to difficult theorems or coming up with new theorems would have endless applications.