Yes, I know AlphaProof did that. I wrote that it would be exciting "if they [LeanDojo] could integrate the reinforcement learning approach from AlphaProof".

This would give LeanDojo a lot more training data, and hopefully give us an open source proof assistant at IMO Silver level.