CMSA New Technologies in Mathematics Seminar: Why explain mathematics to computers?


View Calendar
October 27, 2021 2:00 pm - 3:00 pm
via Zoom Video Conferencing

Patrick Massot - Laboratoire de Mathématiques d’Orsay and CNRS

A growing number of mathematicians are having fun explaining mathematics to computers using proof assistant softwares. This process is called formalization. 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 won't assume any prior knowledge about formalization.