Comment 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.