It's easy to forget, as we all use digital tools in our day-to-day lives, that the world is fundamentally analog, and there's no way to escape that. Everyone trying to tell you otherwise is just selling snake oil, with one notable exception, which is mathematical rigor in proofs. It's understood now that a rigorous proof in math is exactly one that, in principle, can be digitized and checked automatically. Those are simply the same concept, so introducing a computer there is really a perfect fit of tool and purpose. If we can't use computers to automate the checking of mathematical proofs, then why have computers at all? It's the only serious thing people do that a computer can be literally perfect at!

To be clear, there's much more to math than writing down and checking proofs. Some of the most important contributions to math have been simply figuring out the right questions to ask, and also figuring out the useful abstractions. Those are both firmly on the "analog" side of math, and they are every bit as important as writing the proofs. But to say that we have this huge body of rigorous argumentation in math, and then to finally do the work of checking it formally is "taking it too far," is a really bewildering take to me.

No, I don't think formalizing proofs in Lean or other proof systems should dominate the practice of math, and no, I don't think every mathematician should have to write formal proofs. Is that really where we're heading, though? I highly doubt it. The article worries about monoculture. It's a legitimate concern, but probably less of one in math than in many other places, since in my experience math people are pretty independent thinkers, and I don't see that changing any time soon.

Anyway, the conclusion from all this is that the improved ability for mathematicians to rely on automated tools to verify mathematical reasoning would be a great asset. In my opinion the outcomes of that eventuality would be overwhelmingly good.