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 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. Inspired by the theory of programming languages we construe processing of formalized mathematics as a computation whose side effects embody the techniques found in proof assistants, including user interaction, and the computed value a mathematical assertion. These idea provide a basis for the design of a flexible proof assistant that can be extended by the user.
Copyright. All Rights Reserved.
