A growing number of mathematicians are having fun explaining mathematics to computers using proof assistant softwares. This process is called formalization. For instance, together with Kevin Buzzard and Johan Commelin, I recently formalized enough topology and algebra to define Scholze's perfectoid spaces to a computer. In this talk I'll describe what formalization looks like, what kind of things it teaches us, and how it could even turn out to be useful (in our usual sense of "useful"). This will not be a talk about foundations of mathematics, and I will stick to elementary examples.

# Mathematical Conversations

## Mathematics formalization for mathematicians

### Featuring

Patrick Massot

### Speaker Affiliation

Université Paris-Sud

### Affiliation

Mathematics

### Event Series

Date & Time

June 03, 2020 | 5:30 – 7:00pm

### Location

Remote Access Only