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.