The dawn of formalized mathematics

When I was a student of mathematics I was told that someone had formalized an entire book on analysis just to put to rest the question whether mathematics could be completely formalized, so that mathematicians could proceed with business as usual. I subsequently learned that the book was Landau’s “Grundlagen” [6], the someone was L. S. van Benthem Jutting [11], the tool of choice was Automath [12], and that popular accounts of history are rarely correct. Formalized mathematics did not die out. Computer scientists spent many years developing proof assistants [1, 10, 8, 3] – programs that help create and verify formal proofs and constructions – until they became good enough to attract the attention of mathematicians who felt that formalization had a place in mathematical practice. The initial successes came slowly and took a great deal of effort. In the last decade, the complete formalizations of the odd-order theorem [4] and the solution of Kepler’s conjecture [5] sparked an interest and provided further evidence of viability of formalized mathematics. The essential role of proof assistants in the development of homotopy type theory [9] and univalent mathematics [13] showed that formalization can be an inspiration rather than an afterthought to traditional mathematics. Today the community gathered around Lean [3], the newcomer among proof assistants, has tens of thousands of members and is growing very rapidly thanks to the miracle of social networking. The new generation is ushering in a new era of mathematics. Formalized mathematics, in tandem with other forms of computerized mathematics [2], provides better management of mathematical knowledge, an opportunity to carry out ever more complex and larger projects, and hitherto unseen levels of precision. However, its transformative power runs still deeper. The practice of formalization teaches us that formal constructions and proofs are much more than pointless transliteration of mathematical ideas into dry symbolic form. Formal proofs have rich structure, worthy of attention by a mathematician as well as a logician; contrary to popular belief, they can directly and elegantly express mathematical insights and ideas; and by striving to make them slicker and more elegant, new mathematics can be discovered. Formalized mathematics is changing the role of foundations of mathematics, too. A good century ago, a philosophical crisis necessitated the devel-