## Philosophy of Mathematics as a Design Science

In 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.

Reception to follow in in ST 142

**Please register (free) by March 11**

**Jeremy Avigad** is Professor of Philosophy and Mathematical Sciences at Carnegie Mellon University. He has done work in mathematical logic, interactive theorem proving, philosophy of mathematics, history of mathematics, and automated reasoning. He is currently leading the library development for the Lean interactive theorem prover.

*This talk is the fourth annual Calgary Mathematics & Philosophy Lecture, co-sponsored by PIMS, the Pacific Institute for the Mathematical Sciences, and Department of Philosophy and the Department of Mathematics. The Mathematics & Philosophy Lectures aim to introduce topics at the intersection of mathematics and philosophy to a general academic audience. The event is free & open to the public; a reception follows.*