Formalizing invisible mathematics

• 13 February 2023
• Andrej Bauer
• Talks

I am at the Machine assisted proofs workshop at the UCLA Institute for Pure and Applied Mathematics, where I am about to give a talk on “Formalizing invisible mathematics”.

Here are the slides with speaker notes and the video recording of the talk.

Abstract:

It has often been said that all of mathematics can in principle be formalized in a suitably chosen foundation, such as first-order logic with set theory, higher-order logic, or type theory. When one attempts to actually do so on a large scale, the true meaning of the qualifier “in principle” is revealed: mathematical practice consists not only of text written on paper, however detailed they might be, but also of unspoken conventions and techniques that enable efficient communication and understanding of mathematical texts. While students may be able to learn these through observation and imitation, the same cannot be expected of computers, yet.

In this talk we will first review some of the informal mathematical practices and relate them to corresponding techniques in proof assistants, such as implicit arguments, type classes, and tactics. We shall then ask more generally whether these need be just a bag of tricks, or can they be organized into a proper mathematical theory.