Uh no, reinforcemnt learning doesn't magically pop out math proofs. OpenAI has a ton of mathematicians on staff and is spending millions of dollars in compute to pursue these solutions.
That's not necessarily incompatible. The raw output could come from RL rollouts where the model learnt from the process of solving these problems.
Dropping ultra hard problems on those things and giving them reward when lean accepts the proof sound like an obvious RL environment tbh
Then anyone with access to their api’s could’ve come up with these already.
If someone wants to throw enough money at doing that. Solving the Navier-Stokes problem cost a few million dollars. I don't know how much the other problems cost but I suspect they're all above $100.000.
No, because these are not generated using any model available on their api.
So when they release those model, we all will be solving millennium prize problems?
millenium? they'll be solved by then; but hopefully there are some unsolved ones left
Do you foresee that AI will be able to count Rs in strawberry by then?
Jokes aside, by then we're gonna have StarTrek Replicators. Exciting!