Comment by mirashii
1 hour ago
Here's a recent example of an AI exploiting a soundness hole in Lean in a paper purporting to have solved the Collatz Conjecture.
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
There's also a fairly well known incident where the Lean formalization of the Riemann Hypothesis in Mathlib was incorrect.
This paper "purporting to have solved the Collatz conjecture" was essentially a deliberate joke. It was not a serious attempt to prove the Collatz conjecture, it just used that framing to deliberately point out a Lean soundness bug. The soundness bug is real, but the idea that this was something you might accidentally run into while trying to prove the Collatz conjecture is made up.