Philosophy of Mathematics as a Design Science

n the history of philosophy, much has been made of the disagreements between W. V. O. Quine and Rudolf Carnap on the nature of mathematical and scientific knowledge. But when the dust settles, the points of agreement are more substantial: mathematical and scientific reasoning are shaped by the rules of our language, and these rules are, in turn, adopted for pragmatic scientific reasons. In this talk, I will take this perspective seriously, and regard mathematics as a system of conventions and norms that is designed to help us make sense of the world and reason efficiently. Like any designed system, it can perform well or poorly, and the philosophy of mathematics has a role to play in helping us understand the general principles by which it serves its purposes well. To that end, I will consider models of mathematical language currently implemented in interactive theorem provers, which support the formalization and verification of mathematical theorems. Using these models, as well as reflection on ordinary mathematical practice, I will try to extract some insights as to how mathematical language works, and what makes it so effective.