Comment by cma
3 hours ago
Many of the statements were already there and looked over by the community in lean prior to the work though, the statement can get formalized before the proof of it.
3 hours ago
Many of the statements were already there and looked over by the community in lean prior to the work though, the statement can get formalized before the proof of it.
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.
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
2 replies →