News for hackers. Stuff that matters.

A comment on Ask HN: Can we adapt AlphaZero's self-play technique for better human learning?. Parent comment

Re:Ask HN: Can we adapt AlphaZero's self-play technique for ... by ansible on Friday December 08, 2017 @07:18PM (#15883307)
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.

[ Parent | on HN ]
Re:Ask HN: Can we adapt AlphaZero's self-play technique for ... by seanwilson on Saturday December 09, 2017 @04:20AM (#15885000)
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.
[ Parent | on HN ]
Re:Ask HN: Can we adapt AlphaZero's self-play technique for ... by infinity0 on Saturday December 09, 2017 @03:55AM (#15884940)
It's exactly my original point that these goals are not well-defined in early 21st century maths.
[ Parent | on HN ]