Hacker News

points by paxy 3 days ago | 0 comments

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.

[–] baq 3 days ago

Dropping ultra hard problems on those things and giving them reward when lean accepts the proof sound like an obvious RL environment tbh

[–] geraneum 2 days ago

Then anyone with access to their api’s could’ve come up with these already.

[–] mark_something 2 days ago

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.

[–] FuckButtons 2 days ago

No, because these are not generated using any model available on their api.

[–] geraneum 2 days ago

So when they release those model, we all will be solving millennium prize problems?

[–] baq 1 day ago

millenium? they'll be solved by then; but hopefully there are some unsolved ones left

[–] geraneum 1 day ago

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!

[–] Philpax 3 days ago

That's not necessarily incompatible. The raw output could come from RL rollouts where the model learnt from the process of solving these problems.