It is sarcastic. But it is also what OpenAI tried.
The reason they just drop these and say nothing is because these are unverified slop.
OpenAI’s method of verification is rewrite them as Lean proofs that can be verified by computers. Two things have happened so far:
The Lean proof proved the slop wrong, easy, retract.
The Lean proof, being generated by a LLM, is susceptible to hallucinations. For example the Navier Stokes problem Lean proof turned out to be slightly different than the original natural language proof, because the LLM tried to bend a condition to make the proof compile.
But, in case nobody found any problem, OpenAI gets to claim credit for the discovery until someone can review and prove something’s wrong.
You can say these proofs are “Schrodinger’s correct”
Hopefully this is sarcastic
It is sarcastic. But it is also what OpenAI tried.
The reason they just drop these and say nothing is because these are unverified slop.
OpenAI’s method of verification is rewrite them as Lean proofs that can be verified by computers. Two things have happened so far:
But, in case nobody found any problem, OpenAI gets to claim credit for the discovery until someone can review and prove something’s wrong.
You can say these proofs are “Schrodinger’s correct”