BASE DE DONNÉES
DES REVUES DE LA FDE
Liste des revues dépouillées
de la Faculté d'Éducation de l'Académie de Montpellier.
Pour connaître la disponibilité d'un numéro, reportez vous au catalogue BIU
CRD11
CRD30
CRD34
CRD48
CRD66
A partir de cette page vous pouvez :
Retourner au premier écran avec les dernières notices... |
Détail de l'auteur
Auteur Patrick Massot |
Documents disponibles écrits par cet auteur
Affiner la recherche
Pourquoi raconter des mathématiques à un ordinateur / Patrick Massot in La Recherche (Paris. 1970), 571 (10/2022)
[article]
Titre : Pourquoi raconter des mathématiques à un ordinateur Type de document : texte imprimé Auteurs : Patrick Massot Année de publication : 2022 Article en page(s) : p.72-80 Langues : Français Mots-clés : loi et principe scientifique informatique science mathématique 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.
in La Recherche (Paris. 1970) > 571 (10/2022) . - p.72-80[article] Pourquoi raconter des mathématiques à un ordinateur [texte imprimé] / Patrick Massot . - 2022 . - p.72-80.
Langues : Français
in La Recherche (Paris. 1970) > 571 (10/2022) . - p.72-80
Mots-clés : loi et principe scientifique informatique science mathématique 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.