Comment by davidgrenier

I think his argument was restricted to a human-produced mathematical result being ported to a Lean program where one would be just as likely to commit a mistake. However I disagree as well, I recall the difficulty of expressing what I wanted to Coq being a barrier to expressing it incorrectly.