Hmm, am no expert at Lean, but on one hand, since it's a programming language, guessing it necessarily means like all other programming languages, it has bugs.
But on the other hand, agree with you that the chances that one its bugs causes a solved proofs to be wrong is probably very, very low. Yeah, each version of Lean obviously must be run against hundreds if not thousands tests of existing proofs to ensure it's working correctly...
... Although, one thing that is a little worrying is that some mathematicians have said the Lean code generated in these OpenAI proofs is supposedly really complex and undecipherable. It might be pushing Lean to corner cases that are not well tested.
It can possibly have bugs. That said, the "core" of Lean is a somewhat "simple" core that does simple things to check the proof, so it's quite rare to find meaningful bugs
loading story #50329530