Mathematical Practice, Proof Assistants and Meaning

March 13, 2025

Abstract: Twenty-first century mathematics has seen the rise of the proof assistant, and mathematical practice has changed significantly with the rise of these new tools. One consequence of this change, for the philosopher of mathematics, is the wider adoption in mathematics of intuitionistic logic, since many mathematicians now rush to formalise results in the language of constructive type theory (the framework underlying popular proof assistants such as Agda and Lean). In this talk, I will describe this relatively modern phenomenon, and relate it to considerations central to philosophical discussions in the twentieth century, about how to provide a neutral framework for addressing questions in metaphysics. The contemporary use of proof assistants can provide a useful new angle on these longstanding questions, not only about how we can come to know the truths of mathematics, but also for the very content of whatever we can think and say.

This talk is the 2024-2025 Calgary Mathematics & Philosophy Lecture.
The slides for this talk are available here.
Some of the ideas in this talk are discussed in more length in my paper ``What Can We Mean? On Practices, Norms and Pluralisms.''

about

I’m Greg Restall, and this is my personal website. ¶ I am the Shelby Cullom Davis Professor of Philosophy at the University of St Andrews, and the Director of the Arché Philosophical Research Centre for Logic, Language, Metaphysics and Epistemology ¶ I like thinking about – and helping other people think about – logic and philosophy and the many different ways they can inform each other.

To receive updates from this site, subscribe to the RSS feed in your feed reader. Alternatively, follow me at @consequently@hcommons.social, where most updates are posted.

contact

Social media: @consequently@scholar.social.
Personal email: greg@consequently.org.
St Andrews profile.
My office is in Edgecliffe, The Scores.