| ▲ | adgjlsfhk1 7 hours ago |
| 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. |
|
