Rocq has had similar issues with AI finding soundness bugs, particularly in module code last I checked. Yet they don't even have half the resources of Lean. Rocq is nowhere close in my opinion. Though this is really like comparing how many 9s. If Lean is 99.9999% trustworthy, than Rocq is 99.99% trustworthy.
Isabelle/HOL is probably at similar footing to Lean because its kernel is so simple.
Isabelle/HOL is probably at similar footing to Lean because its kernel is so simple.