On: OpenAI withdraws three mathematical results

[viraptor]

> forcing the mathematicians community to do the verification job for them

What do you mean? They're publishing the Lean proofs themselves. Who's forced into anything?

[JohnKemeny → viraptor]

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).

[viraptor → JohnKemeny]

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