Show Notes
There's been a lot of talk recently about whether artificial intelligence is becoming just as good as maths as humans are. But quietly in the background there's been another development regarding the use of computers in maths. It involves proof assistants: computer programmes that can check whether a mathematical proof is correct; whether it can be derived from a set of basic axioms of mathematics using only the rules of logic. In this episode of Living proof we meet Kevin Buzzard, an expert on proof assistants at University College London. Kevin explains what proof assistants are, how using them is like playing a computer game, and why they turn maths into a highly collaborative pursuit. He also tells us about his effort to get a proof assistant to check one of the most famous results in all of mathematics — Fermat's Last Theorem — and how proof assistants and AI may team up to provide a powerful tool. We met Kevin in the summer when he was taking part in a research programme called Big Proof at the Isaac Newton Institute for Mathematical Sciences (INI) in Cambridge. This programme, which attracted some of the best minds in modern mathematics, followed on from a pioneering workshop on the same topic which took place at the INI in 2017. To find out more about the topics mentioned in this podcast, see the following articles:
Proof assistants — This two part article, written by our brilliant summer intern Ben Watkins, is based on the interview with Kevin Buzzard and explores what proof assistants are. Maths in a Minute: Coding with Lean — Here's a simple walk-through of how to use a proof assitant called Lean. Pure maths in crisis? — In this article from 2019 Kevin Buzzard explains why he thinks that the standard of proof in research maths might not be as high as mathematicians would like to believe. How to (im)prove mathematics — This article explores how the simple notion of counting ends in a revolutionary new way of doing maths using proof assistants. This article is based on a talk by Terence Tao at a 2024 workshop at the INI which celebrated the mathematics of Tim Gowers as well as his 60th birthday. A very old problem turns 30! — This article explores Fermat's famous last theorem as well as the mathematics its proof has given rise to. It comes with a podcast featuring Andrew Wiles, who proved the result, and people who are now working on its legacy. You can find more background reading in our collection on proof assistants.
This content forms part of our collaboration with the Isaac Newton Institute for Mathematical Sciences (INI) – you can find all the content from the collaboration here. The INI is an international research centre and our neighbour here on the University of Cambridge's maths campus. It attracts leading mathematical scientists from all over the world, and is open to all. Visit www.newton.ac.uk to find out more.
More from Maths on the Move
Should a life-saving, but expensive, cancer drug be made available on the NHS even though it only benefits very few people? We spoke to Joe Hilton, a health economist, to understand more about how difficult decisions like this one are made.
A family of mathematicians? Learn how one family came together to develop a new proof in group theory.
In this episode, we meet the CEO of one of the most important institutions in mathematics - arXiV. Around since 1991, the website is a publicly accessible home for mathematical research before it is officially published in journals. Around 1,000 articles are published on arXiv every day — it has hosted everything from the proof of the Poincaré Conjecture to some of the newest research from AI companies like DeepSeek and Gemini. We spoke to Ramin Zabih, a Professor at Cornell Tech and Interim Chief Executive Officer at ArXiv, about the organisation and how it supports the very best of mathematical research. Ramin explains why early access is so important, the site’s role in making maths more robust, and why arXiv can publish things that journals can’t. Particularly importantly, he talks about the impact of AI on arXiv’s work. To learn more:
What is the potential of artificial intelligence (AI) in scientific research? In this episode, Cambridge Professor James Fergusson talks about some cutting-edge research which addresses this question. James is Director of the Infosys-Cambridge AI Centre, an innovative partnership between traditional academia and industry. James showed us how AI is quickly becoming the most effective tool for some kinds of data analysis, and even highlighted successful experiments he ran using AI to write research papers. James is also Executive Director of the University of Cambridge's new Master's programme in Data Intensive Science, which is training up the next leaders in the field. He talked us through the programme’s benefits, the institutional approach to AI and the best ways to advance the field. If you'd like to find out more, you might be interested in:
Welcome to the latest episode of Maths on the Move! In this episode we spoke to Cambridge Professor of Theoretical Physics Ulrich Sperhake and his graduate student, Seppe Staelens, about boson stars: hypothetical objects that might be masquerading as black holes. Our conversation with Ulrich and Seppe marked the tenth anniversary of the first detection of gravitational waves. As Ulrich explained back then, gravitational waves "opened our ears to the Universe in a waveband in which we have been 100% deaf up to now" and they also help us understand black holes and boson stars. In this podcast Seppe and Uli explain more, taking us to the frontiers of current research.. To find out more about the topics discussed in this podcast, you might like: