I don't think Lean is as rigorous as you implied here.

https://en.wikipedia.org/wiki/Collatz_conjecture#In_proofs_o...

> In July 2026, a disproof of the Collatz conjecture was verified not only by Lean, but another formal verification system Nanoda. However, investigation quickly revealed that the proof exploited bug(s) in these verifiers.