Repeating the above comment: most of the statements were already formalized prior OpenAI's work. So no, the statements were not "reward hacked".
It doesn't have to be the statement, see the recent incident where someone used an LLM to generate a lean refutation of the collatz conjecture, the lean proof exploited bugs in the lean kernel.
https://lawrencecpaulson.github.io/2026/07/30/Collatz.html
It doesn't have to be the statement, see the recent incident where someone used an LLM to generate a lean refutation of the collatz conjecture, the lean proof exploited bugs in the lean kernel.
https://lawrencecpaulson.github.io/2026/07/30/Collatz.html