How to Formalize All of Mathematics

(This is a guest post, written by Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash and, Adam Topaz.) Mathematicians’ reactions to last week’s big OpenAI release range from excitement to frustration, but one thing is clear: AI has become remarkably good at proving theorems, both formally and informally. The successes in the formal realm have led AI enthusiasts to declare that now is the time to formalize all of mathematics as a legacy for future generations. We are sympathetic to this proposal. We recognize the power of new technologies for mathematical reasoning and appreciate what they can contribute to the subject we know and love. We are generally optimistic about the role AI can play, but we are deeply concerned by some recent calls to formalize everything as quickly as possible. If done well, a large-scale, coordinated formalization effort could enormously expand mathematical exploration and discovery. Done poorly, it will be, at best, a waste…