Repenser les 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 complexe à 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.