| ▲ | mirashii 3 hours 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. | ||
| ▲ | Chinjut 3 hours ago | parent [-] | |
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. | ||