#60 Exploring 'Mathlib' and the digitisation of mathematics: an interview with Professor Kevin Buzzard Artwork

Living Proof: the Isaac Newton Institute podcast

The Isaac Newton Institute is the world's foremost mathematical research centre. Living Proof aims to highlight the diverse people and interconnected topics linked to its many activities. Interviewees range from visiting academics and lecturers to mathematicians, other scientists, musicians, artists, students, and prominent figures within the University of Cambridge and beyond. The podcast typically involves mathematical themes, but is specifically aimed at a general audience. The focus is on the subjects being interviewed and the social stories they have to tell, not just on the significance and details of the research they may be undertaking. We hope there is interest and inspiration here for everyone.- The Isaac Newton Institute for Mathematical Sciences (UK) is an international research centre based in Cambridge, UK. A part of the University of Cambridge, it has been hosting research programmes on mathematical themes since July 1992.Visit > www.newton.ac.uk/news/ini-podcast

All Episodes

Living Proof: the Isaac Newton Institute podcast

#60 Exploring 'Mathlib' and the digitisation of mathematics: an interview with Professor Kevin Buzzard

September 25, 2024 • Isaac Newton Institute for Mathematical Sciences • Episode 60

In the latest episode of Living Proof, Dan Aspel speaks to Professor Kevin Buzzard of Imperial College London. Inspired by a lecture given by Thomas Hales at INI’s Big Proof (https://www.newton.ac.uk/event/bpr/) programme in 2017, Kevin has spent the past seven years working alongside fellow enthusiasts on the “Maths Library” project. In this conversation he explains the project in detail, touching on why the programming language of Lean was chosen, and how it interacts with his recent five-year grant to check the proof of Fermat’s Last Theorem.

If you have been inspired by Kevin’s story, make sure to visit the October 2024 INI research programme Big Specification (https://www.newton.ac.uk/event/bsp/), much of which will be available to watch via live stream on newton.ac.uk

00:00 - Introduction

00:48 - Welcome, explaining the concept behind the “Maths Library”, digitising mathematics

04:20 - “It’s like asking if a submarine can swim”

07:55 - Harnessing the involvement of undergraduates

09:45 - Discussing the motivation, end goals and challenges of the project

17:28 - “The other question is: how far is it going to go? This is an ongoing topic of debate”

20:21 - A minimal, pessimistic prediction of expected progress in 10 years’ time

29:30 - A five-year grant to prove Fermat’s Last Theorem

36:55 - “I’d like to think I’m making the proof of Fermat’s Last Theorem more beautiful”

38:48 - “The goal is to make tools that, together with AI techniques, will turn mathematics on its head”

40:10 - Discussing “Lean” as a functional programming language

44:50 - “The INI Big Proof programme (2017) changed my life completely” (https://www.newton.ac.uk/event/bpr/)

52:50 - “If you hadn’t streamed it, I never would have seen it”, a transformation from a “second-rate number theorist” to business class flights, four-star hotels and chauffeur-driven cars on an international lecture tour

54:48 - “I still wake up every morning thinking ‘I want to prove Fermat’s Last Theorem’”