Mathematical Practice, Proof Assistants and Meaning

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, Prof. Restall 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. 

Greg Restall received his Ph.D. in Philosophy from the University of Queensland in 1994, and before his arrival at the University of St Andrews in 2021, has held positions at the Australian National University, Macquarie University, and the University of Melbourne, where he was Professor of Philosophy since 2013. His research focuses on formal logic, the philosophy of logic, metaphysics, and philosophy of language, and even some philosophy of religion. He has published over 100 papers in journals and collections, and is the author of five books, An Introduction to Substructural Logics (Routledge, 2000), Logic (Routledge, 2006), and Logical Pluralism (Oxford University Press, 2006; with Jc Beall), Proofs and Models in Philosophical Logic (Cambridge University Press, 2022), and Logical Methods (MIT Press, 2023, with Shawn Standefer). His research has been funded by the Australian Research Council, and he is a Fellow of the Australian Academy of the Humanities.

Free and Open to the Public