I just think that with the vast amounts of compute involved and the tendency to reward hack, we can't assume the steps towards that formalization are without error until full human understanding of the formalization.

▲

mkarrmann 5 hours ago | parent [-]

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.