![Iowa Type Theory Commute artwork](https://is2-ssl.mzstatic.com/image/thumb/Podcasts123/v4/48/8e/02/488e02d1-7846-1530-43e4-998ac7b5e423/mza_2593160490166017654.jpg/100x100bb.jpg)
Interjection: The Liquid Tensor Experiment
Iowa Type Theory Commute
English - March 02, 2023 06:00 - 12 minutes - 8.55 MB - ★★★★★ - 13 ratingsTechnology Science Mathematics programming languages computational logic type theory proof assistants cedille Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Previous Episode: Extensional Martin-Loef Type Theory
Next Episode: Introduction to Observational Type Theory
I pause the chapter on extensionality in type theory to talk about something very exciting that I just learned about (though the project was completed Summer 2022): the so-called Liquid Tensor Experiment, to formalize a recent very difficult proof by a mathematician named Peter Scholze, in Lean. This is the first time in history, that I know of, when a theorem was formalized in a theorem prover, in order to resolve doubts of the mathematician who proved it. An amazing achievement. This episode tells the story, as I have understood it on line. The result apparently sparked this recent workshop.