CMSA New Technologies in Mathematics: Breaking the one-mind-barrier in mathematics using formal verification

SEMINARS, CMSA EVENTS

Speaker:

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

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.

For more information on how to join, please see: https://cmsa.fas.harvard.edu/tech-in-math/