Prochain Exposé
Thursday April 8th, 3PM Paris/France. (Playback)
Kevin Buzzard (Imperial College London, UK)
Formalizing 21st century mathematics in Lean. (Slides)
Like it or not, there is snobbery in mathematics. Certain areas are fashionable, and fashions can change. One thing we mathematicians all "know" of course is that mathematics can be done perfectly well with pen and paper (or even papyrus and scrolls), and there is no need for computer proof systems. In 2017 I decided it was time to make "fashionable mathematicians" notice ITPs. Since then I have made a lot of noise and made several big mistakes, but ultimately I hope that I am now on the right path. I will talk about the mathematics people are doing with the Lean theorem prover, and where to go next.
Exposés des semaines suivantes
Vos propositions sont les bienvenues !
