Hear, hear, but the last time I suggested exactly this idea on HN (on a Mochizuki related article IIRC), my comment was downvoted into oblivion by folks who fel

Hear, hear, but the last time I suggested exactly this idea on HN (on a Mochizuki related article IIRC), my comment was downvoted into oblivion by folks who felt I was attacking the "purity" of their trade. To this day, I'm still trying to figure why math types seem to deeply hate the idea that a proper proof of a new theorem should be published in a formal, machine-verifiable language (e.g., Mochizuki's proof, which no one seem to understand, much less verify to be correct, could just be fed to a machine, end of story). I have some hypotheses: 1. Much like "traditional" artists, who saw the Photoshop-like tools as degrading to their art, they feel that using machines to help with proofs would somehow hinder, limit and dirty down their trade. 2. The existing tools are way too primitive to be any kind of useful. This, I can resonate with. I am not knowledgeable enough on current formal proof software, but last I looked at (~10 years ago), they made me feel like I was back to coding in assembly. If indeed the tools are still too primitive, then it's just a matter of making them better. And it seems to me like Math, if anything, really lends itself damn well to hierarchical building to reach better and better level of abstraction. 3. Many folks mix-up automated theorem proving (which is hard for machines, because it requires intuition leaps) and formal proof verification (which, unless I'm missing something, really lends itself well to mechanization). Anyhoo, I suspect that in spite of all the philosophical push-back, we will get there, if only because many modern proofs are so huge, they get to the point where they consume multiple mathematician-lifetimes worth of work. There's basically no other route.