Πηγαίνετε εκτός σύνδεσης με την εφαρμογή Player FM !
Interjection: The Liquid Tensor Experiment
Manage episode 356777645 series 2823367
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.
165 επεισόδια
Manage episode 356777645 series 2823367
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.
165 επεισόδια
Όλα τα επεισόδια
×Καλώς ήλθατε στο Player FM!
Το FM Player σαρώνει τον ιστό για podcasts υψηλής ποιότητας για να απολαύσετε αυτή τη στιγμή. Είναι η καλύτερη εφαρμογή podcast και λειτουργεί σε Android, iPhone και στον ιστό. Εγγραφή για συγχρονισμό συνδρομών σε όλες τις συσκευές.