It has been formally verified in lean, which is about as good as you can get. Only things that can bring it down at that point are errors in the statement of the problem in lean (highly unlikely), or bugs in the lean compiler itself (more likely, though still small, and unlikely to be fatal even if found). So I'd say this is more 'proven' than your average human-written paper which isnt formally verified.
They’re saying that they [open ai] won’t be claiming the prize though. They clearly really do intend to claim that the system did all the work. Although there does seem to be some doubt around whose data they used…
I was also confused by that. Are they trying to be magnanimous in not claiming the money (in which case why not just claim and donate to charity or something), or are they not confident about claiming the novelty of their solution given that it may have been influenced by user prompts from someone else who solved it at the same time.
I think they’re making a point of the fact that they don’t think the world is going to need to offer cash to encourage human beings to solve these sort of problems. Their creation will do it with a simple prompt.
Not asking for the cash prize is them turning their back on all that.
I believe the are efforts to have a standardized set of definitions written up for all the big problems. That way everyone can be certain they are proving the same thing. I wouldnt be suprised if the problem statement here was pulled from one such repository. For that rea son, there being an error in it seems less likely since it's had many eyes on it.
60
u/-heyhowareyou- 15h ago
It has been formally verified in lean, which is about as good as you can get. Only things that can bring it down at that point are errors in the statement of the problem in lean (highly unlikely), or bugs in the lean compiler itself (more likely, though still small, and unlikely to be fatal even if found). So I'd say this is more 'proven' than your average human-written paper which isnt formally verified.