undefined | Better HN

0 pointsinfinity08y ago0 comments

What are the winning conditions for math?

0 comments

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.

In 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.

infinity0OP8y ago

It's exactly my original point that these goals are not well-defined in early 21st century maths.

j / k navigate · click thread line to collapse

0 comments

ansible8y 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.

seanwilson8y ago

infinity0OP8y ago

It's exactly my original point that these goals are not well-defined in early 21st century maths.

j / k navigate · click thread line to collapse