|
Action Concertée Incitative Nouvelles Interfaces des Mathématiques |
|
|
Projet Mao -- Mathématiques assistées par ordinateur |
|
|
1- Le caractère innovant du projet La communauté mathématique commence seulement à prendre lentement conscience de l'aide considérable que peut lui apporter l'ordinateur. Jusqu'ici les assistants de preuve ont été développés sans contact suffisant avec la recherche mathématique de pointe. L'innovation ne réside donc pas dans la pratique de mathématiques formelles, déjà bien rodée, mais dans le projet d'adapter cette pratique au niveau de la recherche de pointe.
2- La valeur ajoutée par la coopération Nous pensons que l'outil informatique qu'utiliseront les mathématiciens ne peut être conçu qu'en collaboration étroite entre des professionnels des assistants de preuves, des professionnels des interfaces, et des mathématiciens professionnels. Notre projet réunit ces trois types de compétences.
3- L'intérêt du projet pour les applications La principale application que nous visons est l'utilisation des ordinateurs par les chercheurs en mathématiques. Mais qui peut le plus peut le moins: l'environnement que nous allons produire, ou des environnements dérivés seront appréciés partout où l'on fait des preuves: en informatique théorique, dans l'enseignement des mathématiques et dans les secteurs de pointe de l'industrie. Nous pensons que l'ordinateur va progressivement modifier en profondeur le métier de mathématicien. Cette modification va être progressive, comme ça s'est passé pour Tex, avec des pionniers, et avec une vitesse de diffusion très variable selon la discipline. Nous sommes également convaincus que les doctorants joueront un rôle décisif dans le développement et la diffusion de la nouvelle pratique. Les mathématiques récentes comportent trop souvent une masse décourageante de détails techniques sans grand intérêt. Ce constat vaut autant dans des disciplines comme la géométrie algébrique ou la topologie algébrique, où l'on manipule de plus en plus systématiquement des structures de plus en plus sophistiquées, que dans des disciplines comme la géométrie 2D ou 3D, où l'on ne manipule pourtant que des objets élémentaires. En géométrie 2D et 3D, on connait bien les exemples du problème des quatre couleurs et de la conjecture de Kepler (à laquelle est consacré le projet Flyspeck mentionné plus haut). Pour un exemple frappant en topologie algébrique, voir la thèse de Régis Péllissier (disponible sur la page web de Carlos Simpson) qui démontre un théorème fondamental assurant que les catégories de Segal forment une catégorie de modèles; la preuve de ce théorème prend trois cents pages et si les experts peuvent bien en comprendre la ligne générale, aucun n'a ni le temps ni l'envie d'en vérifier les détails; ce travail de vérification sera certainement fait pour la première fois par un ordinateur, vraisemblablement guidé par un ou plusieurs mathématiciens débutants ou retraités. Nous pensons qu'il est grand temps de rendre possible l'utilisation massive des ordinateurs dans la recherche mathématique et voulons précipiter l'avènement (au demeurant inéluctable) de la future façon de rédiger/formuler/pratiquer les mathématiques. Passons maintenant en revue les tâches "subalternes" que l'ordinateur accomplira à la place du mathématicien. a) l'ordinateur garantira la correction des preuves. On connait bien les limites du processus d'arbitrage par les pairs. Citons l'exemple frappant du "théorème" de Roos de 1961, auquel Neeman a opposé un contre-exemple en 2003 dans Inventiones Mathematicae, b) l'ordinateur complètera les détails des preuves et fera de plus en plus de calculs; le mathématicien pourra de plus en plus se concentrer sur les choix cruciaux de la preuve. c) l'ordinateur assistera également le mathématicien dans la recherche de la preuve, par exemple en faisant des calculs ou encore en présentant de façon intelligente (à la google) les ressources pertinentes, d) l'ordinateur s'occupera de l'édition des preuves ("proof by pointing"). Insistons sur le fait qu'il ne s'agit pas d'une vue de l'esprit. Notre nouvelle interface permet de résoudre en une vingtaine de clics des exercices de première année comme par exemple "Prouver que l'image d'une réunion est la réunion des images". Il reste bien sûr à changer d'échelle d'une part et aussi à concevoir un langage de sortie plus convivial et naturel que le vernaculaire de Coq. Nous considérons le premier point comme capital. Quant au second, bien qu'il soit moins urgent, nous avons embauché Philippe Audebaud (ENS Lyon) pour amorcer une réflexion à son propos. En effet, dans un travail antérieur, Audebaud a montré qu'il est possible d'extraire d'une preuve Coq un article LATEX certifié. Son analyse fait ressortir la nécessité de disposer d'un format de communication des données entre le prouveur et la machine graphique. Il envisage d'aborder ce travail par la spécification d'une API, qui serait évidemment utile dans tous les compartiments de notre projet et au-delà. (dernière mise à jour du site : 14 décembre 2004) |
|
|
|
|