Comment by JohnKemeny
1 day ago
They are not publishing Lean proofs. They are publishing proofs in natural language, and are not submitting to journals.
They are just putting out a bunch of weirdly written extremely long and technical papers and saying: Hey, here is the solution (we hope there are no mistakes).
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