This is the home page for a seminar that was taught by Jeremy Avigad (avigad@cmu.edu) at Carnegie Mellon in the fall of 2015. The course numbers were 80-513/813.
The seminar met on Fridays from 10:00 to 12:20 in Baker Hall 150, the Philosophy Department Seminar Room.
The first meeting will be held on Friday, September 4.
The bibliography below provides a sense of what we will read. But the bibliography will grow over the coming weeks, and the actual readings will depend on the interests of the participants.
In this seminar we will think about mathematics in fairly syntactic terms, as a body of norms and conventions that govern the practice of the subject. The advent of computational proof assistants, which use stylized languages to convey mathematical content, provides new perspectives on these norms and conventions. This seminar will consider ways that these formal models of mathematical language and inference can be brought to bear on traditional and contemporary questions in the philosophy of mathematics.
The strategy we will adopt is to think of mathematics as a system that is designed to help us to make sense of the world and reason effectively. Like any designed system, it can perform well or poorly, and our goal will be to understand the general principles by which such a system serves our purposes well. We will consider both informal and formal mathematics, and explore the extent to which formal models of mathematics can help clarify the goals, values, and methods of the informal practice.