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

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.

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.