Page 52 - 8th European Congress of Mathematics ∙ 20-26 June 2021 ∙ Portorož, Slovenia ∙ Book of Abstracts
P. 52
INVITED SPEAKERS
The dawn of formalized mathematics
Andrej Bauer, Andrej.Bauer@andrej.com
University of Ljubljana, Slovenia
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 construc-
tions – 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 gath-
ered 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 development of logic and set theory, which
served as the bedrock upon which the 20th century mathematics was built safely. However,
most proof assistants shun logic and set theory in favor of type theory, the original resolution of
the crisis given by Bertrand Russell [14] and reformulated into its modern form by Per Martin-
Löf [7]. The reasons for this phenomenon are yet to be fully understood, but we can speculate
that type theory captures mathematical practice more faithfully because it directly expresses the
structure and constructions of mathematical objects, whereas set theory provides plentiful raw
material with little guidance on how mathematical objects are to be molded out if it.
References
[1] S.F. Allen, M. Bickford, R.L. Constable, R. Eaton, C. Kreitz, L. Lorigo, and E. Moran.
Innovations in computational type theory using Nuprl. Journal of Applied Logic, 4(4):428–
469, 2006.
[2] Jacques Carette, William M. Farmer, Michael Kohlhase, and Florian Rabe. Big math and
the one-brain barrier – the tetrapod model of mathematical knowledge. Mathematical In-
telligencer, 43(1):78–87, 2021.
50
The dawn of formalized mathematics
Andrej Bauer, Andrej.Bauer@andrej.com
University of Ljubljana, Slovenia
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 construc-
tions – 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 gath-
ered 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 development of logic and set theory, which
served as the bedrock upon which the 20th century mathematics was built safely. However,
most proof assistants shun logic and set theory in favor of type theory, the original resolution of
the crisis given by Bertrand Russell [14] and reformulated into its modern form by Per Martin-
Löf [7]. The reasons for this phenomenon are yet to be fully understood, but we can speculate
that type theory captures mathematical practice more faithfully because it directly expresses the
structure and constructions of mathematical objects, whereas set theory provides plentiful raw
material with little guidance on how mathematical objects are to be molded out if it.
References
[1] S.F. Allen, M. Bickford, R.L. Constable, R. Eaton, C. Kreitz, L. Lorigo, and E. Moran.
Innovations in computational type theory using Nuprl. Journal of Applied Logic, 4(4):428–
469, 2006.
[2] Jacques Carette, William M. Farmer, Michael Kohlhase, and Florian Rabe. Big math and
the one-brain barrier – the tetrapod model of mathematical knowledge. Mathematical In-
telligencer, 43(1):78–87, 2021.
50
