Résumé
Il existe un écart important entre la notion formelle de preuve et le genre d’argument qui passe généralement pour une preuve dans la littérature mathématique. Souvent, cela ne crée aucune difficulté, mais cet écart est devenu de plus en plus marqué à mesure que les preuves dans la littérature sont devenues de plus en plus compliquées. L’intervenant est une figure de proue dans le domaine de la formalisation, c’est-à-dire de l’activité qui consiste à écrire des preuves de manière qu’elles puissent être vérifiées mécaniquement par un ordinateur. Le séminaire a porté sur les attitudes à l’égard de la preuve et sur la façon dont elles peuvent changer.
