How to Formalize All of Mathematics

Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash and Adam Topaz have written a blog post over on Kevin Buzzard’s blog entitled “How to Formalize All of Mathematics”, regarding recent proposals to automatically formalize the entirety of the mathematical literature. The issues regarding formal mathematics are parallel to those regarding informal mathematics, in particular the tradeoff between speed, scale, and understanding when one prioritizes the production of output over all other desiderata, and the blog post is largely focused on this tradeoff.