That, or an error in the specification (ie.: not the implementation).
(I very much am with you that his attitude / way of framing it is a bit weird)
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).