Comment by mistercheph

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