Orateur
Description
L’ordinateur est une machine capable d’exécuter précisément un algorithme donné. Cela en fait naturellement un outil mathématique. Je parlerai en particulier de deux rôles:
- Vérifier des preuves formelles. C’est le principe des assistants de preuves qui sont le thème de ces journées.
- Effectuer des calculs complexes, numériques ou symboliques, qui sont hors de portée de l’humain.
Nous regarderons comment certains formalismes, comme la théorie des types sous-jacente à Rocq et Lean, permet de concilier ces deux aspects à travers des preuves comportant une part de calcul importante.
Parmi ces preuves, il y a le théorème des quatre couleurs, dont nous présenterons quelques aspects.
Dans une dernière partie, je présenterai des travaux plus récents sur une interface graphique et gestuelle pour construire des preuves formelles de manières (parfois) plus rapide ou intuitive. Ces travaux ouvrant, je l’espère, des pistes nouvelles pour la pédagogie des mathématiques.