I'm not saying that starting 2024, journals should only start accepting formalized proofs. I'm well aware that we're probably many thousands of person years awa

I'm not saying that starting 2024, journals should only start accepting formalized proofs. I'm well aware that we're probably many thousands of person years away from being able to formalize research involving modern mathematical objects like rough paths or perfectoid spaces. But I do think that we should be moving in that direction. We're halfway through formalizing undergrad education, once we're there we could start including it in graduate courses, and at some point we'll have caught up. Many thousands of years of work divided by many thousands of active grad students maybe isn't prohibitively much. I don't see a reason why in some future, something like Lean couldn't replace something like LaTeX as the de-facto standard language for communicating mathematics. We could build the papers directly from source with docstrings. I don't even think that it would replace peer review, since this considers at least three things, correctness, novelty and relevance, roughly in that order, but it could make it substantially easier by automating much of the first part. And I think it might make the paper writing itself more efficient and enjoyable as well.