BROADCASTS.com

b'

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.\\xa0 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.\\xa0 An amazing achievement.\\xa0 This episode tells the story, as I have understood it on line.\\xa0 The result apparently sparked this recent workshop.