Comment by paxy
8 hours 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.
8 hours 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.
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.
[dead]
That's not necessarily incompatible. The raw output could come from RL rollouts where the model learnt from the process of solving these problems.