Comment by baq
6 hours ago
Dropping ultra hard problems on those things and giving them reward when lean accepts the proof sound like an obvious RL environment tbh
6 hours ago
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.
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.
[dead]