The Liquid Tensor Experiment

Add to your list(s) Download to your calendar using vCal

• Professor Kevin Buzzard (Imperial College London)
• Thursday 02 February 2023, 17:00-18:00
• Centre for Mathematical Sciences MR12, CMS.

If you have a question about this talk, please contact Angeliki Koutsoukou-Argyraki.

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?

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• Centre for Mathematical Sciences MR12, CMS
• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• 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
• bld31
• yk449

Note that ex-directory lists are not shown.