Comment by viraptor

They're doing both. Some results were initially published without Lean. But they continue adding the proofs where they're missing: https://github.com/openai/math/tree/main/lean