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 7 hours ago | parent [-]

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

▲

paxy 5 hours ago | parent [-]

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 2 hours ago \| parent \| next [-]
		Dropping ultra hard problems on those things and giving them reward when lean accepts the proof sound like an obvious RL environment tbh
	▲	Philpax 5 hours ago \| parent \| prev [-]
		That's not necessarily incompatible. The raw output could come from RL rollouts where the model learnt from the process of solving these problems.