"Elements of Mathematics" in the Digital Age#

Marc Bezem#

Abstract

Euclid's "Elements" have undoubtedly been 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 (1918-2012). 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 from mathematical-proofs-as-social-constructs to full accountability. We present an overview of recent projects in computer-verified mathematics and discuss how this development can lead to a cultural change in mathematical research and education.