| Titre : | Pourquoi raconter des mathématiques à un ordinateur (2022) |
| Auteurs : | Patrick Massot |
| Type de document : | Article : texte imprimé |
| Dans : | la Recherche (Paris. 1970) (571, 10/2022) |
| Article en page(s) : | p.72-80 |
| ISBN/ISSN/EAN : | 0029-5671 |
| Langues de la publication : | Français |
| Descripteurs | |
| 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 |
Exemplaires (1)
| Code-barres | Cote | Support | Localisation | Section | Disponibilité |
|---|---|---|---|---|---|
| 7676 | archives | Périodique | CDI | Périodiques | Disponible |
Peut-être aimerez-vous
 L'informatique in Textes et documents pour la classe (1975), 997 (01/06/2010) | Maths informatique in La Recherche. Hors-série (2015), 033 (03/2020) | SNT et documentationFlorie Delacroix in Inter CDI (Etampes), 282 (11/2019) |  Une histoire de records in 01net, 1032 (09/10/2024) |  L'expérimentation scientifiqueGuy Belzane in Textes et documents pour la classe (1975), 1010 (15/02/2011) |  Informatique MP2I, MPI 1re et 2e années : cours et exercices corrigésThibault Balabonski (DL 2022) |