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

Page: https://stenobird.com/podcast/living-proof-the-isaac-newton-institute-podcast-5453937/60-exploring-mathlib-and-the-digitisation-of-mathematics-an-interview-with-professor-kevin-buzzard
Text version: https://stenobird.com/podcast/living-proof-the-isaac-newton-institute-podcast-5453937/60-exploring-mathlib-and-the-digitisation-of-mathematics-an-interview-with-professor-kevin-buzzard.md
Podcast: [Living Proof: the Isaac Newton Institute podcast](https://stenobird.com/podcast/living-proof-the-isaac-newton-institute-podcast-5453937)
Published: 2024-09-25T08:00:00+00:00
Episode link: https://www.buzzsprout.com/1992011/episodes/15806373-60-exploring-mathlib-and-the-digitisation-of-mathematics-an-interview-with-professor-kevin-buzzard.mp3
Audio file: https://www.buzzsprout.com/1992011/episodes/15806373-60-exploring-mathlib-and-the-digitisation-of-mathematics-an-interview-with-professor-kevin-buzzard.mp3
Processing state: not_requested
JSON: https://stenobird.com/v1/public/podcasts/living-proof-the-isaac-newton-institute-podcast-5453937/episodes/60-exploring-mathlib-and-the-digitisation-of-mathematics-an-interview-with-professor-kevin-buzzard
Duration seconds: 3335

## Resource

Send us Fan Mail 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 ...

## Actions

- request_transcript: `POST https://stenobird.com/v1/public/podcasts/living-proof-the-isaac-newton-institute-podcast-5453937/episodes/60-exploring-mathlib-and-the-digitisation-of-mathematics-an-interview-with-professor-kevin-buzzard/transcription-requests` — Idempotently request low-priority transcript generation for this episode.
- read_markdown: `GET https://stenobird.com/podcast/living-proof-the-isaac-newton-institute-podcast-5453937/60-exploring-mathlib-and-the-digitisation-of-mathematics-an-interview-with-professor-kevin-buzzard.md` — Read the agent-friendly Markdown representation of this episode resource.

A page view does not enqueue transcription. Agents should invoke `request_transcript` explicitly when they need this episode processed.

## Transcript

Full transcripts are not published on public pages unless there is a clear rights basis.