Why do you assume this order? I would assume the AI starts with lean (that's what it was RL'd on at least) then tried to translate the proof for us humans, which is quite hard.

I'm not sure about it but it seems plausible given the potential error.

Edit: they explicite say that your order is correct in the post