The Liquid Tensor Experiment
- đ¤ Speaker: Professor Kevin Buzzard (Imperial College London) đ Website
- đ Date & Time: Thursday 02 February 2023, 17:00 - 18:00
- đ Venue: Centre for Mathematical Sciences MR12, CMS
Abstract
In July 2022 a team led by Johan Commelin and Adam Topaz completely formalised in Lean the proof of a theorem of Dustin Clausen and Peter Scholze. Scholze described the result by saying “I think this may be my most important theorem to date”. What is the point of formalising it, what did it teach us, and what happens next?
Series This talk is part of the Formalisation of mathematics with interactive theorem provers series.
Included in Lists
- All CMS events
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Centre for Mathematical Sciences MR12, CMS
- CMS Events
- Department of Computer Science and Technology talks and seminars
- DPMMS info aggregator
- DPMMS lists
- DPMMS Lists
- DPMMS Pure Maths study groups
- Formalisation of mathematics with interactive theorem provers
- Hanchen DaDaDash
- Interested Talks
- Martin's interesting talks
- School of Physical Sciences
- School of Technology
- Trust & Technology Initiative - interesting events
- yk449
Note: Ex-directory lists are not shown.
![[Talks.cam]](/static/images/talkslogosmall.gif)



Thursday 02 February 2023, 17:00-18:00