Pourquoi raconter des mathématiques à un ordinateur / Patrick Massot / Sophia Publications (2022) in La Recherche (Paris. 1970), 571 (10/2022)

Public ISBD Aucun avis sur cette notice. [article]  inLa Recherche (Paris. 1970) > 571 (10/2022) Titre : Pourquoi raconter des mathématiques à un ordinateur Type de document : texte imprimé Auteurs : Patrick Massot Editeur : Sophia Publications, 2022 Article : p.72-80 Langues : Français (fre) Descripteurs : informatique Mots-clés : science mathématique  loi et principe scientifique 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. Nature du document : documentaire Genre : Article de périodique [article] Pourquoi raconter des mathématiques à un ordinateur [texte imprimé] / Patrick Massot . - Sophia Publications, 2022 . - p.72-80. Langues : Français (fre) in La Recherche (Paris. 1970) > 571 (10/2022) Descripteurs : informatique Mots-clés : science mathématique  loi et principe scientifique 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. Nature du document : documentaire Genre : Article de périodique