En direct
Best of
Best of du 7 au 13 septembre
En direct
Flash-actu
Articles populaires
Période :
24 heures
7 jours
01.

600 milliards perdus pour cause de mauvais investissements : mais au fait, quels sont les placements intelligents simples à mettre en place ?

02.

Le management vertical a tendance à fatiguer de plus en plus les salariés

03.

L'Ifop révèle une enquête sur la population musulmane en France

04.

Alerte mondiale : cette déconnexion croissante (et inquiétante) de l’économie réelle et des marchés financiers

05.

La France est-elle menacée par des attaques "non-attribuables" comme en a connues l’Arabie saoudite sur ses champs de pétrole ?

06.

Jerôme Fourquet mesure l'empreinte grandissante de l'Islam sur le quotidien; Valeurs Actuelles tente de mesurer le lien entre fraude sociale et immigration; Chez LR on ne veut pas de primaire ouverte (sauf Retailleau); Chez LREM on redoute les municipales

07.

Véhicules propres : la Chine abandonne l'électrique pour miser sur la voiture à hydrogène

01.

Patrick Bruel : une deuxième masseuse l'accuse ; Adieu Sebastien Farran, bonjour Pascal, Laeticia Hallyday retrouve enfin l’amour ! ; Lily-Rose Depp & Timothée Chalamet squelettiques mais heureux, Céline Dion juste maigre...;

02.

Retraites : ces trois questions pièges souvent oubliées des grands discours

03.

Laeticia Hallyday aurait retrouvé l’amour

04.

L'Ifop révèle une enquête sur la population musulmane en France

05.

Les avantages et les bienfaits d'une éducation conservatrice pour nos enfants face à la faillite éducative contemporaine

06.

Ces 3 questions pièges de tout débat sur l’immigration en France

01.

Patatras : l’étude phare qui niait l’existence de notre libre arbitre à son tour remise en question

02.

Selon le président la Conférence des Évêques de France, les citoyens "inquiets" du projet de loi bioéthique ont le "devoir" de manifester le 6 octobre

03.

Ces 3 questions pièges de tout débat sur l’immigration en France

04.

Pourquoi LREM pourra difficilement échapper à son destin de “parti bourgeois” quels que soient ses efforts

05.

PMA / GPA : la guerre idéologique est-elle perdue ?

06.

Marine Le Pen : retour aux fondamentaux (et au plafond de verre)

ça vient d'être publié
pépite vidéo > Justice
Japon
Fukushima : trois anciens dirigeants de Tepco ont été acquittés
il y a 10 heures 4 min
pépites > Environnement
Emploi du temps
Ségolène Royal, ambassadrice des pôles, n'aurait pas assisté aux réunions du Conseil de l'Arctique
il y a 10 heures 54 min
light > Justice
Butin important
Les propriétaires du château de Vaux-le-Vicomte ont été séquestrés
il y a 12 heures 32 min
décryptage > Culture
Atlanti-Culture

"LECTURES D'ETE": Notre sélection des meilleurs livres des 10 derniers mois, "L'amour est aveugle" de William Boyd

il y a 13 heures 58 min
pépites > Politique
Victoire ?
Procès de Jean-Luc Mélenchon : le renvoi du parquet a été refusé
il y a 14 heures 48 min
décryptage > Sport
LDC

PSG - REAL : 3 - 0 Sans ses stars mais avec un Idrissa Gueye impérial, Paris surclasse le Real de Zidane

il y a 17 heures 36 min
décryptage > Economie
Vie professionnelle

Le management vertical a tendance à fatiguer de plus en plus les salariés

il y a 18 heures 9 min
décryptage > France
Riposte

Recrudescence des mites mangeuses de vêtements à cause des fibres naturelles et du lavage à basse température

il y a 18 heures 41 min
décryptage > Politique
Langue de bois s'abstenir

Une étude des universités de Harvard et de Berkeley démontre qu’en politique les propos clivants et politiquement incorrects paient

il y a 19 heures 16 min
décryptage > Economie
Atlantico Business

Alerte mondiale : cette déconnexion croissante (et inquiétante) de l’économie réelle et des marchés financiers

il y a 19 heures 55 min
pépites > International
Tunisie
Mort de l'ancien président tunisien Ben Ali
il y a 10 heures 31 min
light > Société
Vocation
Traverser la rue pour trouver un emploi : la nouvelle vie de Jonathan
il y a 11 heures 42 min
pépite vidéo > International
Campagne
"Blackface" : Justin Trudeau présente ses excuses après la diffusion d'une photo polémique
il y a 13 heures 33 min
pépites > Santé
Mesures
Un rapport parlementaire dévoile la prise en charge "catastrophique" des patients en psychiatrie
il y a 14 heures 9 min
décryptage > High-tech
Le monde d’après Snowden

Mémoires de Snowden : mais où en est-on de la surveillance mondiale à l’heure actuelle ?

il y a 17 heures 5 min
décryptage > Santé
Santé

L’imposture psychosomatique comme prétendu diagnostic (de secours) de maladies complexes

il y a 17 heures 45 min
décryptage > Economie
Epargne

600 milliards perdus pour cause de mauvais investissements : mais au fait, quels sont les placements intelligents simples à mettre en place ?

il y a 18 heures 28 min
décryptage > Politique
Évaporation du domaine de la lutte

L’autre gros problème de Jean-Luc Mélenchon

il y a 19 heures 44 sec
décryptage > Défense
La guerre à l’heure des ennemis non identifiés

La France est-elle menacée par des attaques "non-attribuables" comme en a connues l’Arabie saoudite sur ses champs de pétrole ?

il y a 19 heures 32 min
rendez-vous > Media
Revue de presse des hebdos
Jerôme Fourquet mesure l'empreinte grandissante de l'Islam sur le quotidien; Valeurs Actuelles tente de mesurer le lien entre fraude sociale et immigration; Chez LR on ne veut pas de primaire ouverte (sauf Retailleau); Chez LREM on redoute les municipales
il y a 20 heures 6 min
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.
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.

600 milliards perdus pour cause de mauvais investissements : mais au fait, quels sont les placements intelligents simples à mettre en place ?

02.

Le management vertical a tendance à fatiguer de plus en plus les salariés

03.

L'Ifop révèle une enquête sur la population musulmane en France

04.

Alerte mondiale : cette déconnexion croissante (et inquiétante) de l’économie réelle et des marchés financiers

05.

La France est-elle menacée par des attaques "non-attribuables" comme en a connues l’Arabie saoudite sur ses champs de pétrole ?

06.

Jerôme Fourquet mesure l'empreinte grandissante de l'Islam sur le quotidien; Valeurs Actuelles tente de mesurer le lien entre fraude sociale et immigration; Chez LR on ne veut pas de primaire ouverte (sauf Retailleau); Chez LREM on redoute les municipales

07.

Véhicules propres : la Chine abandonne l'électrique pour miser sur la voiture à hydrogène

01.

Patrick Bruel : une deuxième masseuse l'accuse ; Adieu Sebastien Farran, bonjour Pascal, Laeticia Hallyday retrouve enfin l’amour ! ; Lily-Rose Depp & Timothée Chalamet squelettiques mais heureux, Céline Dion juste maigre...;

02.

Retraites : ces trois questions pièges souvent oubliées des grands discours

03.

Laeticia Hallyday aurait retrouvé l’amour

04.

L'Ifop révèle une enquête sur la population musulmane en France

05.

Les avantages et les bienfaits d'une éducation conservatrice pour nos enfants face à la faillite éducative contemporaine

06.

Ces 3 questions pièges de tout débat sur l’immigration en France

01.

Patatras : l’étude phare qui niait l’existence de notre libre arbitre à son tour remise en question

02.

Selon le président la Conférence des Évêques de France, les citoyens "inquiets" du projet de loi bioéthique ont le "devoir" de manifester le 6 octobre

03.

Ces 3 questions pièges de tout débat sur l’immigration en France

04.

Pourquoi LREM pourra difficilement échapper à son destin de “parti bourgeois” quels que soient ses efforts

05.

PMA / GPA : la guerre idéologique est-elle perdue ?

06.

Marine Le Pen : retour aux fondamentaux (et au plafond de verre)

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 !