Living Proof: Kevin Buzzard and proof assistants

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.