Por Luís Cruz-Filipe (Department of Mathematics and Computer Science, University of Southern Denmark).

The proof of the four-color theorem in 1976 is usually referenced as the birth of computer-assisted mathematical proofs, although some earlier examples exist. Since then, computers have slowly started working their way into mathematicians' toolboxes; and the relevance of computers for mathematical proofs was confirmed with the inclusion of a panel discussion on the topic at ICM 2018.

In this talk we discuss the logical foundations of computer proofs and what it means to say that a theorem has been proved with the help of a computer. We cover some recent examples from combinatorics and number theory, and discuss ongoing work around the topic of session types.

This is a joint session with SAL (CMA/FCT-UNL).

Zoom | ID da reunião: 890 8479 3299 - senha de acesso: 409604