Time: Tuesday 01.12, 14.15–15.00

Room: C115, Kronstad

Speaker: Marc Bezem, UiB.

Title: “Elements of mathematics” in the digital age


“Elements of Mathematics” is the title of some grand endeavors in the foundations of mathematics. Euclid’s “Elements” have undoubtedly be the most influential, followed at a certain distance by Bourbaki. Less well known, but also potentially influential, is the “Elements”-like project Automath by N.G. de Bruijn.

The essence of this (and more recent) projects is the ultimate formalization of mathematics, to the extent that mathematical prose (definitions, theorems, proofs) becomes machine-processable. Independent verification of proofs by a computer constitutes a transition of mathematical-proofs-as-social-constructs to full accountability. We discuss how this development can lead to a cultural change in research and education in mathematics.