On the other hand, if you want full and complete rigor that means formalizing things in a computer-based proof checker. Now, that can often reveal ways to refactor the argument into a cleaner, more elegant, more intuitive proof, which is why full formalizations are often regarded as publishable work - but the other side of it is that dotting all the i's and crossing all the t's does take a whole lot of effort since some published proofs are not nearly as clear as they're supposed to be.
I agree that some published proofs are not as clear as they're supposed to be, but I disagree that formalizing things in computer-based proof checkers is the way forward there. Computer proof checking is cool, but its an augment to what we already do and not not a substitute for it.
The purpose of a published paper is to explain things to other humans, while that of a computer formalization is to explain things to computers. Just as it is generally not easy for a computer to understand a published proof, it is usually not easy for other mathematicians to understand the code you feed to Lean or whatever.
The stuff you need to focus on to get a computer to accept your proof is usually quite different to the stuff you want to focus on when explaining things to colleagues. Roughly speaking we care about why you're doing things, while the computer cares about the intricacies of what you're doing.
