Prof. Andrej Bauer (Photo: Marko Cokan - Foto Kozama)
Publish Date: 28.10.2021
Category: Researchers in focus , Our contribution to sustainable development goals
Sustainable development goals: 4 Quality education (Indicators)
Andrej Bauer, professor of computational mathematics at Faculty of Mathematics and Physics, University of Ljubljana, will be awarded by the American Mathematical Society (AMS) in 2022 the Levi L. Conant Prize for the article “Five stages of accepting constructive mathematics. The Prize recognizes the best expository paper published in either the Notices of the AMS or the Bulletin of the AMS in the preceding five years. The prize will be presented January 5 at the 2022 Joint Mathematics Meetings in Seattle.
Bauer's article is an introduction to constructive mathematics, which differs from its classical counterpart in that it abandons Aristotle’s law of the excluded middle. For a long time it has been considered a marginal field, studied by a relatively small number of mathematicians. Lately constructive mathematics has found its anchorage in computer science, because all proofs, calculations and constructions carried out constructively can be systematically transformed into computer programmes. (For example, a constructive proof of the existence of a solution to a differential equation at the same time enables us to solve the equation with a computer.) In the recent decades, mathematicians and computer scientists have developed computer tools based on this idea, which can be used to create programs whose correctness can be formally verified with a computer.
As noted in the AMS announcement of the prize, Bauer begins his article by recalling the basic premise of constructive mathematics—namely, that one gives up the law of excluded middle—then quickly clears up several common confusions. He explains Diaconescu's result that the axiom of choice implies excluded middle before proving that excluded middle is equivalent to the statement that subsets of finite sets (in the constructivist sense) are finite. The article gently introduces some of the basic ideas of constructivism. It leads the reader on the first few baby steps of doing constructivist mathematics, where subtle changes in the statement of a theorem (otherwise indistinguishable from a non-constructivist viewpoint) make a significant difference.
Many mathematicians display a skepticism or even hostility towards constructivism. Bauer's article directly addresses such readers and takes them on a guided tour through the garden of constructive mathematics. While most mathematicians are unlikely to fundamentally change the way they do mathematics after reading this article, there are very few who will not have their eyes opened to a way of thinking they may not have otherwise appreciated—even on issues they thought they already understood. This is all accomplished with a deft sense of humor and patience. This is an article whose ideas will stay with the reader long after it has been read.
Response from Andrej Bauer upon reciving the award:
»I am truly honored and grateful to receive the 2022 Levi L. Conant Prize. I thank the AMS for recognizing the effort invested into the article, and the editor Mark Goresky for kind and sustained encouragement that kept me going until the article took an acceptable form. This is also a good opportunity to state my gratitude to the small but resilient constructive mathematics community, which has given me far more than I could ever give back.
I first came into contact with constructive mathematics during my graduate years, while studying computability in analysis and topology. I still remember how difficult it was to learn constructive thinking and to suppress the instincts distilled into me by classical mathematical training. When I became a teacher, I enjoyed explaining constructive mathematics to students, colleagues, and strangers on the Internet. With time, I got better at helping them overcome common stumbling blocks and purge misconceptions that impeded their intuitions. The article “Five stages of accepting constructive mathematics” is the synthesis of these experiences, as well as an honest disclosure of my personal views on constructive mathematics and mathematics in general.«
Biographical Sketch of Andrej Bauer:
Andrej Bauer is a professor of computational mathematics at the Faculty of Mathematics and Physics of the University of Ljubljana. In 1994 he received his Sc.B. in Mathematics from Ljubljana, and in 2000 he received his PhD in Pure and Applied Logic from Carnegie Mellon University under the supervision of Dana S. Scott. In 2001, he spent a semester at the Mittag-Leffler Institute in Stockholm, Sweden. In 2012, he was a fellow at the Institute for Advanced Study, where he contributed to the development of homotopy type theory. Bauer’s work spans foundations of mathematics, constructive and computable mathematics, type theory, homotopy type theory, and mathematical principles of programming languages. He is an author of the book “Homotopy Type Theory: Univalent Foundations of Mathematics” and the initiator of the HoTT library, an extensive formalization of homotopy type theory in the Coq proof assistant. He is also known for his seminal work on programming with algebraic effects and handlers. Lately he has been working on type theory and the design of proof assistants.
Bauer also presents mathematics to the broader public, while his interests outside mathematics include computer-generated art and aikido, for which he has the title of a master. We also kindly invite you to watch Bauer’s lecture “Five Stages of Accepting Constructive Mathematics” at the Institute for Advanced Study, which was the basis for the prize-winning article.
*The text is largely based on the text published on AMS site: https://www.ams.org/news?news_id=6827
Algebraic numbers (by Andrej Bauer)
Algebraic numbers are complex numbers that are the roots of polynomial equations with integer coefficients. The figure shows algebraic numbers that are the roots of polynomials of degree up to 5. The color represents the degree of the polynomial and the radius represent the size of its coefficients. There are a total of 10469668 algebraic numbers in the figure. The picture was part of an exhibition organized by the Faculty of Mathematics and Physics at the Jakopič Avenue in Tivoli Park (Ljubljana) in 2019, on the occasion of the 100th anniversary of the University of Ljubljana.