Patrick Massot
Pourquoi raconter des maths aux ordinateurs ?
De plus en plus de mathématiciens s’amusent en expliquant des mathématiques aux ordinateurs via des logiciels appelés assistants de preuves. Dans cet exposé j’expliquerai à quoi ressemble ce processus, dit de formalisation, quel genre de choses il nous apprend et comment il pourrait même s’avérer utile (en notre sens habituel du mot « utile »).
- ANNÉE 2021-2022
- Séminaire Des mathématiques