|
Résumé :
|
Le point sur l'intervention des ordinateurs en mathématiques dans la résolution des théorèmes, leur communication et leur enseignement. Face à la complexité des théorèmes, les ordinateurs interviennent comme "assistant de preuve". Plus récemment, développement des "bibliothèques" de mathématiques fondamentales, fichiers informatiques regroupant de très nombreuses définitions et démonstrations pouvant être utilisées ensemble. Exemple de la conjoncture de Kepler résolue avec le logiciel HOL Light. Impossibilité d'automatiser la formalisation qui nécessite de longues étapes fastidieuses. Différences d'approches entre mathématiciens et informaticiens. Mise au point de bibliothèques numériques de démonstrations pour les grands projets de formalisation. Logiciel Lean, projet de logiciel libre. Si les ordinateurs ont malgré tout parfois une efficacité limitée, ils restent un atout pour la partie technique. Possibilité d'expliquer des mathématiques avec un degré de précision inédit. Comment la démonstration permet de valider la cohérence entre l'intuition, les définitions et les énoncés. Encadrés : le défi des mathématiques condensées ; dialogue avec un assistant de preuve.
|
