Comment by raincole

The answer is we don't really know [0]:

> In 2026, AIs designed to spot bugs in software were directed at Lean, and found several loopholes which were then fixed. Perhaps related to this effort, a purported disproof of the Collatz conjecture was announced as verified in Lean. However, this proof was soon determined to rely on a bug in Lean, and once the bug was fixed the proof was found invalid

However it's a bit different than the usual 'bugs' we encounter in normal software development. Lean is more like a type checker. If you can write a false proof in Lean then the bug is in Lean itself, not your code.

In other words, Lean can have bugs, but the amount of code we need to check scales with Lean itself, not with the length of proof. Just like the chance that C compiler has bugs doesn't increase as we write more C code. So the 13M lines of code doesn't really matter here.

[0]: https://en.wikipedia.org/wiki/Lean_(proof_assistant)