The Future of Mathematics?

Abstract: I will talk about the state of the art of so-called “proof assistants”, computer systems which right now are pretty much incapable of assisting any mathematician with any serious proof. However, these proof assistants can do something. In fact over the last few years the Lean proof assistant has been taught a lot of undergraduate and MSc algebra, analysis, number theory, geometry and topology. I will give a live demonstration showing what Lean can do now, and then talk about what proof assistants might soon be able to do, and speculate about how they might be useful to mathematicians in the future.

Mathematics

Audience: researchers in the discipline

Barcelona Mathematical Days 2020

Series comments: Note that registration is free but mandatory, and available until Oct 22nd.

All the events will be streamed via Zoom but only registered participants will receive the connection details.

Visit bmd2020.espais.iec.cat for more details.