University of Cambridge > > Formalisation of mathematics with interactive theorem provers  > The Liquid Tensor Experiment

The Liquid Tensor Experiment

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity