Dropping ultra hard problems on those things and giving them reward when lean accepts the proof sound like an obvious RL environment tbh