Comment by mistercheph
3 hours ago
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.
3 hours ago
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.
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.