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’”