Atlantico, c'est qui? c'est quoi ?
Mercredi 25 Mai 2016 | Créer un compte | Connexion
Extra

Comment les ordinateurs font voler en éclats les règles fondamentales des mathématiques

Le médaillé Fields de 2002 souhaite repenser les théories des mathématiques qui font aujourd'hui autorité, afin de vérifier certains théorèmes devenus trop complexes à résoudre pour l'homme.

Vous allez adorer les maths

Publié le - Mis à jour le 5 Juin 2015
Comment les ordinateurs font voler en éclats les règles fondamentales des mathématiques

Les ordinateurs font voler en éclats les règles fondamentales des mathématiques.

Le médaillé Fields (plus haute distinction en mathématiques) 2002, Vladimir Voedovski, souhaite confier les mathématiques à l'informatique. Cette initiative pourrait-elle amener à repenser les théories mathématiques actuelles ? Arrivera-t-on à traduire les mathématiques dans un langage que l'ordinateur comprendra ?

Pierre-Louis Curien : Je commencerai par préciser que l'ordinateur ne pense rien. On souhaite néanmoins rendre les mathématiques suffisamment explicites pour que l'ordinateur puisse vérifier que toutes les règles de raisonnement utilisées ont été utilisées correctement.

On souhaite demander à l'ordinateur de vérifier ce qu'on lui demande de vérifier. Pour cela, il faut donc lui mâcher le travail. On lui parle déjà dans une langue plus proche des mathématiques que du langage machine. C'est tout le travail d'un logiciel comme Coq. Le logiciel Coq permet d'exprimer les démonstrations dans un langage qui reste proche de la pensée du mathématicien, mais quand même encore assez loin pour que l'exercice reste très difficile. Le mathématicien qui s'oblige à vérifier sa preuve par l'informatique se doit donc d'être plus explicite que dans son langage courant de mathématicien, et c'est une première difficulté majeure.

Le logiciel Coq est très utilisé par certains mathématiciens, comme Vladimir Voedovski. Il aimerait que beaucoup plus de gens l'utilise, et souhaiterait ainsi que le logiciel soit plus simple à utiliser. Aujourd'hui par exemple, on sait formaliser en Coq de l'algèbre, et non de l'analyse, qui est une partie très importante des mathématiques.

Par ailleurs, la deuxième difficulté réside dans le fait que toutes les notions que l'on utilise doivent être comprises par l'ordinateur, donc expliquées. Pour faire de la géométrie par exemple, nous nous devons de reconstruire sur l'ordinateur tous les axiomes sur lesquels la géométrie repose. En ce sens, c'est un peu reprendre les mathématiques à partir de zéro. 

Pourquoi ce scientifique s'est-il lancé dans cette initiative ? Quel est ce courant de pensée ? D'où proviennent ces chercheurs ?

Vladimir Voedovski, lors de certains articles et de démonstrations scientifiques, a découvert une erreur assez importante dans l’un de ses articles, pourtant publié, et donc accepté par les relecteurs, qui sont d’autres mathématiciens. Il en est arrivé à la conclusion que certaines théories mathématiques sont devenues tellement complexes qu'on ne pourra plus détecter les erreurs, et que l'Homme ne pourra plus vérifier la véracité de certains systèmes. Il a donc souhaité généraliser les assistants de preuve, afin de pouvoir considérer les preuves comme correctes quand l'ordinateur les acceptera. Sa motivation est avant tout personnelle.

Habitant à Princeton, il a consulté certains spécialistes et s'est penché sur le logiciel Coq. Il s'est également penché sur la théorie sur laquelle le logiciel Coq est fondé : la théorie des types, une sorte d'alternative à la théorie des ensembles. Il a trouvé il y a quelques années une extension de la théorie des types, qui s'appelle la théorie homotopique des types, qu'il a découverte il y a quelques années. Avec cette nouvelle théorie, il a l'impression que l'on peut plus facilement parler de théories mathématiques, que ce que permettait la fondation classique des mathématiques à travers la théorie des ensembles. Jusqu'à il y a une dizaine d'années, on considérait que la théorie des ensembles était la fondation des mathématiques. Sans parler de révolution, la théorie des types étendue par Voevodski semble plus  naturelle et efficace pour formaliser les mathématiques sur l’ordinateur.

J'aimerais enfin rappeler que le courant de pensée est principalement européen. La théorie des types comme le logiciel Coq est le fruit de travaux de théoriciens travaillant en France, en Angleterre, en Ecosse, en Suède. Voevodski, qui travaille sur le logiciel Coq, travaille sur un produit français. Son extension est une avancée fascinante, qui donne un nouveau souffle aux mathématiques et des fondations un peu différentes… et prometteuses. 

Quels intérêts pourrait-on trouver dans la refonte de ces théories mathématiques ? Quel pourrait être l'impact d'une telle découverte ? Peut-on espérer des avancées pour la science, l'astronomie, l'Histoire ?

Ce nouvel effort de fondation ne risque pas tant de bouleverser l’édifice de la recherche mathématique elle-même que la façon de travailler des mathématiciens. Ce qui est important, si ces fondations réussissent, c'est que le travail mathématique sera plus facile à formaliser. Le fait d'avoir remplacé des fondations de la théorie des ensembles par la théorie des types étendue va faciliter le travail du mathématicien quand il travaillera avec un ordinateur.

Je ne pense pas que ces avancées auront un impact immédiat et significatif sur d'autres sciences. Très indirectement, si un logiciel comme Coq devient plus facilement utilisable, il pourra aussi servir à certifier des langages de programmation, des logiciels embarqués, qui mettent en jeu notre sécurité. D'une manière générale, Coq pourra nous servir à avoir des logiciels plus sûrs, et trouvera une utilité pour la sûreté de voitures autonomes, d'avions, etc.

Un très bel exemple a déjà été fourni par la certification complète d’un compilateur du langage C  réalisée à l’INRIA  et achevée il y a deux ans, par Xavier Leroy et ses collaborateurs (projet CompCert). Cette réalisation a reçu en 2011 le prix  La Recherche en sciences de l’information.

 
Commentaires

Nos articles sont ouverts aux commentaires sur une période de 7 jours.
Face à certains abus et dérives, nous vous rappelons que cet espace a vocation à partager vos avis sur nos contenus et à débattre mais en aucun cas à proférer des propos calomnieux, violents ou injurieux. Nous vous rappelons également que nous modérons ces commentaires et que nous pouvons être amenés à bloquer les comptes qui contreviendraient de façon récurrente à nos conditions d'utilisation.

  • Par LouisArmandCremet - 03/06/2015 - 11:34 - Signaler un abus Analyse vs Algèbre..

    Quand on réfléchit un peu, on voit vite que l'analyse n'est qu'un cas particulier dans R de l'algèbre. Je ne comprends pas pourquoi l'analyse tient le haut du pavé alors qu'il y a tant de choses fascinantes en algèbre !

  • Par Henrik Jah - 03/06/2015 - 12:01 - Signaler un abus A Louis Armand

    L'analyse tient le haut du pavé car ça rapporte plus d'argent tout simplement! :) Enfin pour l'instant... Sujet passionnant.

  • Par VV1792 - 03/06/2015 - 23:41 - Signaler un abus Sujet passionnant, Mr Currien

    Sujet passionnant, Mr Currien ne fait pas dans le sensationnel, et communique des informations completement meconnues du public, meme pour ceux ayant un peu de culture mathematique. Les mathematiques en France ont longtemps ete de tres haute valeur.. il faut souhaiter que cela perdure..

Pour commenter :

Depuis son lancement Atlantico avait fait le choix de laisser ouvert à tous la possibilité de commenter ses articles avec un système de modération a posteriori. Sous couvert d'anonymat, une minorité d'internautes a trop souvent détourné l’esprit constructif et respectueux de cet espace d’échanges. Suite aux nombreuses remarques de nos lecteurs, nous avons décidé de réserver les commentaires à notre communauté d’abonnés.

Pierre-Louis Curien

Pierre-Louis Curien est directeur de recherche au CNRS. Ancien élève de l’Ecole Normale Supérieure, et après des études de mathématiques, il a fondé en 1999 le laboratoire Preuves, Programmes et Sytèmes (CNRS et Université Paris Diderot), et dirige maintenant au sein de ce laboratoire une équipe commune INRIA (nommée pi;r2) qui pilote le développement du logiciel Coq et mène des études théoriques autour de ce logiciel.

Voir la bio en entier

Je m'abonne
à partir de 4,90€