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
don't disbelieve you, but just looked at the reference language, it seems pretty full featured as a programming language, even with basic classes, polymorphism, scope, namespaces... But maybe most of the mathematicians who actual code with stick with the simpler language features? And also, didn't look to deeply, these could be very simple features that actually aren't very sophisticated.
loading story #50329946