En direct
Best of
Best of du 12 au 18 janvier
En direct
Les ordinateurs font voler en éclats les règles fondamentales des mathématiques.
Vous allez adorer les maths
Comment les ordinateurs font voler en éclats les règles fondamentales des mathématiques
Publié le 05 juin 2015
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.
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...
Suivre
Vous devez être abonné pour suivre un auteur.
Abonnez-vous
«Vos abonnements garantissent notre indépendance»
Pierre-Louis Curien
Suivre
Vous devez être abonné pour suivre un auteur.
Abonnez-vous
«Vos abonnements garantissent notre indépendance»
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...
Voir la bio
Ajouter au classeur
Vous devez être abonné pour ajouter un article à votre classeur.
Abonnez-vous
«Vos abonnements garantissent notre indépendance»
Lecture Zen
Vous devez être abonné pour voir un article en lecture zen.
Abonnez-vous
«Vos abonnements garantissent notre indépendance»
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.

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.

Les commentaires de cet article sont à lire ci-après
Articles populaires
Période :
24 heures
7 jours
01.
L'étonnante proposition de Brigitte Macron à Valérie Trierweiler et Carla Bruni-Sarkozy
02.
Plus court mais mieux indemnisé : cette réforme de l’assurance chômage qui pourrait offrir une solution aux demandeurs d’emplois
03.
Connaissez vous Marie Kondo (la Japonaise qui a déclenché une folie du rangement dans le monde qui ne devrait pas tarder à atteindre la France) ?
04.
Glyphosate : l’incroyable manque de rigueur scientifique d’Envoyé Spécial
05.
Changement climatique : Alexandria Ocasio-Cortez déclare que "le monde touchera à sa fin dans 12 ans"
06.
Ce biais statistique qui explique pourquoi la redistribution en France est loin d’être aussi efficace qu’on le croyait pour corriger les inégalités
07.
La tombe de Marc Antoine et Cléopâtre serait sur le point d'être découverte
01.
Glyphosate : l’incroyable manque de rigueur scientifique d’Envoyé Spécial
02.
Plus court mais mieux indemnisé : cette réforme de l’assurance chômage qui pourrait offrir une solution aux demandeurs d’emplois
03.
Comment le Canard Enchaîné a envoyé François Fillon, Jacques Chaban-Delmas et Valéry Giscard d'Estaing au cimetière des éléphants de la politique
04.
Jacques Chirac, ce soudard amateur de bières et de belles femmes qui s'est avéré être un excellent chef des armées
05.
Connaissez vous Marie Kondo (la Japonaise qui a déclenché une folie du rangement dans le monde qui ne devrait pas tarder à atteindre la France) ?
06.
Traité d’Aix-la-Chapelle : la France ne vend pas l’Alsace à l’Allemagne mais les deux pays scellent la coupure entre les dirigeants et leurs peuples
07.
La tombe de Marc Antoine et Cléopâtre serait sur le point d'être découverte
01.
Glyphosate : l’incroyable manque de rigueur scientifique d’Envoyé Spécial
02.
Réponse à tout… sauf aux Gilets jaunes ? Pourquoi l’intelligence de Macron participe plus du problème que de la solution à la crise de défiance qui ébranle la société française
03.
Traité d’Aix-la-Chapelle : la France ne vend pas l’Alsace à l’Allemagne mais les deux pays scellent la coupure entre les dirigeants et leurs peuples
04.
Les patrons américains préfèrent la France de Macron à l’Amérique de Donald Trump et l’idée du « grand débat » leur plait
05.
Aix-la-Chapelle ou la dernière illustration en date de l’intimidation morale qui asphyxie la démocratie française
06.
La tombe de Marc Antoine et Cléopâtre serait sur le point d'être découverte
01.
Réponse à tout… sauf aux Gilets jaunes ? Pourquoi l’intelligence de Macron participe plus du problème que de la solution à la crise de défiance qui ébranle la société française
02.
Glyphosate : l’incroyable manque de rigueur scientifique d’Envoyé Spécial
03.
Gilets jaunes : l’inexplicable (et énorme) échec des Républicains
04.
Aix-la-Chapelle ou la dernière illustration en date de l’intimidation morale qui asphyxie la démocratie française
05.
Radioscopie des dépenses de la France : ces nouvelles inégalités qui se cachent derrière la puissance apparente de l'État-providence
06.
Emmanuel Macron est brillant, mais il n’est pas le président qu’il faut à la France
Commentaires (3)
Ecrire un commentaire
Vous devez être abonné pour rédiger un commentaire.
Abonnez-vous
«Vos abonnements garantissent notre indépendance»
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.
*Toute validation est définitive, vous ne pourrez pas rééditer votre commentaire.
VV1792
- 03/06/2015 - 23:41
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..
Henrik Jah
- 03/06/2015 - 12:01
A Louis Armand
L'analyse tient le haut du pavé car ça rapporte plus d'argent tout simplement! :) Enfin pour l'instant... Sujet passionnant.
LouisArmandCremet
- 03/06/2015 - 11:34
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 !