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

That's not necessarily incompatible. The raw output could come from RL rollouts where the model learnt from the process of solving these problems.