Comment by siknad

OpenAI having NL proofs earlier than Lean ones would require trust in the proof without ability to check it automatically. Perhaps Lean proofs are published later because it is considered a less important implementation detail or because there is a cleanup step that takes time.