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.