Loading Events

« All Events

  • This event has passed.

Breaking the one-mind-barrier in mathematics using formal verification

September 14, 2022 @ 2:00 pm - 3:00 pm

New Technologies in Mathematics Seminar

Speaker: Johan Commelin, Mathematisches Institut, Albert-Ludwigs-Universität Freiburg

Title: Breaking the one-mind-barrier in mathematics using formal verification

Abstract: In this talk I will argue that formal verification helps break the one-mind-barrier in mathematics. Indeed, formal verification allows a team of mathematicians to collaborate on a project, without one person understanding all parts of the project. At the same time, it also allows a mathematician to rapidly free mental RAM in order to work on a different component of a project. It thus also expands the one-mind-barrier.

I will use the Liquid Tensor Experiment as an example, to illustrate the above two points. This project recently finished the formalization of the main theorem of liquid vector spaces, following up on a challenge by Peter Scholze.



September 14, 2022
2:00 pm - 3:00 pm
Event Category:


Michael Douglas


CMSA Room G10
CMSA, 20 Garden Street
Cambridge, MA 02138 United States
+ Google Map