Repeating the above comment: most of the statements were already formalized prior OpenAI's work. So no, the statements were not "reward hacked".

▲

mistercheph 4 hours ago | parent [-]

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

	▲	Jtarii 4 hours ago \| parent \| next [-]
		That proof was artificially constructed specifically to show the exploit. It wasn't a real attempt at a proof that was later shown to be using an exploit. I'm unaware of any serious proofs that have been shown to have a kernel exploit in them.
	▲	mkarrmann 3 hours ago \| parent \| prev [-]
		That's a different argument than ijustlovemath is making I agree with Jtarii that it's very unlikely a Lean bug is critical to most of these proofs. But we're in strange times, so I agree wtih the sentiment that we should wait for further analysis before declaring complete confidence in the proofs.