Hacker News

points by softwaredoug 3 days ago | 0 comments

I wonder how long it'll pay for frontier labs to use compute this way?

I'm reminded of the Apollo program that was cool for a while, but eventually the public lost interest.

Maybe it becomes cheaper? Maybe other labs want to prove their worth will pick up the slack when another loses interest?

[–] adgjlsfhk1 3 days ago

the presumption is that these results are a side-effect of reinforcement learning to make the models smarter.

[–] paxy 3 days ago

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

[–] 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.