Pourquoi raconter des maths aux ordinateurs ?
amphi Galois NIRPatrick 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 »).