My claim is not that nobody ever makes mistakes, it’s formalizing in a computer is extremely high cost for very little reward and doesn’t help the core process of finding proof ideas

And Kevin Buzzard (who is an established algebraic number theorist) is making the claim that this no longer applies in a world where people are depending on 1000-page proofs that maybe two people have ever checked. In the case of Jim Arthur's work, zero people have checked it, because Arthur hasn't even finished writing it down, yet people are publishing results that depend on it.