La formalisation est un processus qui consiste à utiliser l’ordinateur non pas pour calculer mais pour raisonner. Il est en train de devenir un outil puissant pour aider les mathématiciens et mathématiciennes dans leur travail de recherche. En effet, il est aujourd’hui possible de formaliser un résultat récent en un temps raisonnable, et les choses ne peuvent que s’améliorer dans les années à venir. Dans cet exposé, je vais décrire le processus de formalisation, avec des nombreux exemples, et je vais expliquer pourquoi ça peut être utile en mathématiques, dans le sens usuel du terme.

L’ensemble des membres du laboratoire est cordialement invité.