alt Hacker NewsThe way to tame a profit-maximizer is to make the most profitable choice the one that creates the most societal good.
I would like to see the Clay Institute give zero recognition for formalizations without human-readable proofs. That would incentivize OpenAI to scram or create something that's actually useful.
Replies
Jblx2 • today at 4:03 AM
OpenAI has already said they aren't going to claim the $1,000,000. If this proof claim holds up, then the Millennium prizes will be 2 for 2 for rejections of the prize money for valid solutions. Maybe that will be the precedent for other AI labs as well.
It would be trivially easy to convert Lean into English, so I’m not sure what the human-readable criteria gets you. There are also human written proofs that are considered not human-readable by most of the mathematics community (ABC conjecture).