I will go further (since there are certainly bugs in the kernels of proof assistants, more frequently than you might imagine). Even if there is a bug in Lean's

I will go further (since there are certainly bugs in the kernels of proof assistants, more frequently than you might imagine). Even if there is a bug in Lean's kernel, it will almost never invalidate a Lean proof, because bugs in the Lean kernel (or the kernels of other proof assistants) are, just like with normal programs, almost always bugs dealing with edge cases testing the boundaries of mathematics or syntax, not things that show up in everyday proofs. Coq has fixed numerous proofs of False and, to my knowledge, these fixes have never ended up invalidating a "real" proof that wasn't specifically designed to test these kinds of edge cases. Proofs are far more often broken by changes to the surface syntax (e.g. inference algorithms or the tactic language) than by changes to the kernel. Obviously, this is not foolproof against malicious "adversarial" mathematicians, so knowing something was proved in Lean still requires some degree of checking. But it does make it pretty extraordinarily unlikely that a false proof in a proof assistant was arrived at by accident, which is far from the case with the "old" way of doing mathematics. (I'd also add that the concern about getting the specification of a design wrong is something that rarely lasts longer than attempts to actually use it to prove anything nontrivial, since the proofs won't go through, but there at least can be a lot of debate about how to interpret specifications in some fields [e.g. computer science] or whether certain specs are "actually" equivalent to the statements someone wants to prove, especially for stuff like category theory where manual proofs have a good deal of handwaving... but these are minor technical issues compared to the viewpoint of the article).