I don't think Lean is as rigorous as you implied here.
replyhttps://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.
Doesn't Lean also have libraries? Anyway, there could also be hardware errors, I suppose.
replyLean does have libraries, but since they are also in lean they are subject to the same rules. It's basically a super strong type checker. If it compiles the proof is valid. Unless there is a bug in the type checker.
replyWhy should you trust that the relatively small core of Lean is correct?
replyThe core of Lean got a lot less correct when a well-meaning AI system probed Lean for corner cases (bugs) that would "prove" a false conjecture. Corner cases so arcane that no human exploit in a proof. Basically, humans are too stupid to break human-created Lean, but the AI is not.