Introduction aux mathématiques formalisées

Mardi 7 mai 13:00-15:00 - Patrick Massot - LMO

Résumé : Dans cet exposé-TP, j’essaierai de répondre à quelques questions qui
m’ont été posées durant des pauses café récentes : que signifie « expliquer
une définition ou une démonstration mathématique à un ordinateur » ?
Est-ce faisable sans formation en logique ou informatique ?
Cela pourrait-il être utile aux mathématiciens ? Peut-on l’utiliser pour
enseigner ?
Dans un premier temps, je ferai un exposé sur ces questions, en
m’appuyant sur l’exemple de la définition des espaces perfectoïdes,
expliquée très récemment aux ordinateurs, et sur des exemples
de cours en L1 utilisant la vérification de démonstrations par
ordinateur, à Londres et à Orsay. Il n’est pas nécessaire de savoir ce
qu’est un espace perfectoïde ou un étudiant de L1, je ferai des rappels.
Dans un deuxième temps, je guiderai l’auditoire pour écrire ses
premières définitions et démonstrations formalisées.
Note : La partie TP requiert de se connecter aux machines des salles
informatique de notre bâtiment.
=============

Lieu : 0D10

Introduction aux mathématiques formalisées  Version PDF