OpenAI Pulls Three Math Proofs Over a Sign Error

OpenAI, the company behind ChatGPT, has withdrawn three proofs from its math project on GitHub, the platform where it stores the code and papers. A sign error in one paper broke the argument that two other proofs depended on. The team fixed 14 more papers. It also updated the citation links in 13 other papers. Formalization means rewriting a proof so a computer can check every step. Coverage in the project now stands at 300 out of 719 results, or about 42 percent.

The same pattern shows up in software written by AI agents. A result can look finished. One wrong step can still be hiding somewhere in the middle of the work. The error only surfaces when someone checks the reasoning step by step. That is why someone other than the agent itself should check its output before release.