Les mathématiques sur de nouvelles bases

Une véritable révolution se prépare-t-elle dans les mathématiques ? Un bouleversement qui changerait fondamentalement la manière dont les mathématiques sont pratiquées ? Dans un avenir proche, est-ce que ce sont les ordinateurs plut?t que les hommes qui vérifieront de manière fiable si une preuve mathématique est correcte ?

Si l'on suit la blogueuse Julie Rehmeyer, le mathématicien russe Vladimir Vo?evodski (*1966), professeur à l'Institute for Advanced Studies de Princeton, a effectivement développé une approche qui pourrait révolutionner les mathématiques et leurs fondements : En principe, le mathématicien russe a pu montrer que la théorie de l'homotopie, qui traite de la déformation d'objets géométriques, exprime les mêmes idées que la théorie des langages de programmation et la logique mathématique, mais dans un autre langage (la théorie de l'homotopie a joué un r?le central dans les travaux du Russe sur la conjecture de l'homotopie).sur la conjecture de Milnor, pour laquelle il a re?u la prestigieuse médaille Fields en 2002), écrit-elle dans un blog de la revue de vulgarisation scientifique "Scientific American".

Wojewodski lui-même veut réunir deux axes de développement des mathématiques actuelles. Pour qu'il puisse présenter ses idées en personne à Zurich, l'ETH l'a invité en septembre à être l'intervenant des "Paul Bernays Lectures 2014". Giovanni Felder, le directeur de l'Institut d'études théoriques de l'ETH (ITS), présentera ses recherches au public de l'ETH. Il explique : "Wojewodski développe une nouvelle théorie qui place les mathématiques sur de nouvelles bases. Les questions qu'il soulève concernent aussi bien les fondements des mathématiques que ceux de l'informatique et de la logique". Cette théorie s'appelle "Théorie des types d'homotopie (HoTT)" et "Fondements univalents des mathématiques" le projet correspondant, axé sur l'informatique.

Une langue simplifiée pour les preuves informatiques

Dans le cadre de "HoTT", Vladimir Vo?evodski développe une approche qui permet de traduire des preuves mathématiques beaucoup plus facilement qu'aujourd'hui dans un langage de programmation d'assistants de preuve informatiques (en anglais "proof assistants"). Si cette approche fait ses preuves, les ordinateurs pourraient à l'avenir examiner des preuves aussi compliquées, dans lesquelles même les mathématiciens les plus chevronnés commettent des erreurs. "Avec l'aide d'assistants de preuve, nous pourrions former des théories mathématiques très complexes et très abstraites", explique Wojewodski.

Pour les mathématiciens, de tels assistants de preuve ne seraient pas une chose secondaire, car d'une part la preuve est en quelque sorte leur technique clé, et d'autre part les assistants de preuve exigent de nouvelles bases en mathématiques. Tout d'abord, pour être acceptées, les preuves en mathématiques doivent être correctes et respecter les règles logiques. Leur exactitude doit pouvoir être déduite sans erreur et à partir de certains principes vrais (axiomes) et d'énoncés déjà prouvés. Le rêve de nombreux mathématiciens a toujours été de formuler les axiomes à partir desquels toutes les propositions mathématiques peuvent être déduites et prouvées sans contradiction.

La théorie des ensembles est difficile à traduire

Ernst Zermelo a présenté un tel système d'axiomes en 1908. Il est aujourd'hui connu sous le nom d'axiomatique de Zermelo-Fraenkel de la théorie des ensembles et sert également de fondement à l'ensemble des mathématiques, car tous les objets mathématiques peuvent également être interprétés comme des ensembles.

L'inconvénient de la théorie des ensembles est que ses principes sont très difficiles à traduire dans le langage de programmation d'un assistant de preuve. Les programmes de preuve existants aujourd'hui, comme le "coq" utilisé par Wojewodski, reposent donc sur la théorie des types , proposée par le mathématicien et philosophe anglais Bertrand Russell (1872-1970) comme alternative à la théorie des ensembles.

Ce qui est innovant dans l'approche de Wojewodsky, c'est qu'il interprète les énoncés du système formel de la théorie des types dans le langage de la théorie de l'homotopie. Dans cette interprétation s'applique alors une propriété supplémentaire, appelée univalence, que Wojewodski ajoute comme nouvel axiome aux fondements des mathématiques. Il y met en relation l'égalité des énoncés logico-mathématiques avec l'équivalence au sens de la théorie de l'homotopie.

Tasse et beignet : un langage plus riche

Cette approche peut para?tre surprenante au premier abord, car la théorie de l'homotopie s'intéresse en fait à la manière dont on peut transformer différents objets géométriques les uns dans les autres par des déformations. Une tasse et un beignet illustrent bien cette théorie : du point de vue de leur forme, ils ont l'air complètement différents. Cependant, au vu de leurs propriétés, ils sont tous deux un "objet avec une ouverture". Le beignet est un anneau et la tasse a une anse. De plus, la tasse peut être transformée en beignet de telle sorte que les points qui sont adjacents sur la tasse le sont également sur le beignet. Les deux objets intuitivement différents ont donc des propriétés identiques. Ils sont équivalents ou équivalents, comme disent les mathématiciens.

Ce problème d'équivalence se pose également lors de l'interprétation des équations utilisées en mathématiques et dans les langages de programmation. Une équation telle que "a=b" est un énoncé mathématique dans lequel deux symboles différents ont la même valeur. Cela correspond logiquement à deux formes différentes ayant des propriétés structurellement identiques.

Même idée, différentes langues

"Gr?ce à Wojewodski, nous savons maintenant que l'on peut mieux formuler de telles relations d'égalité dans la théorie de l'homotopie, car c'est une théorie plus riche", explique Giovanni Felder. La théorie de l'homotopie explique non seulement pourquoi "a est égal à b", mais aussi comment on peut aller de a à b. Dans la théorie des ensembles, il faudrait en plus définir cette information, ce qui complique la traduction des phrases mathématiques dans le langage de programmation, explique Felder : "L'espoir est qu'avec la méthode de Wojewodski, on puisse traduire plus directement les preuves dans le langage de programmation et les vérifier plus efficacement".

? la question de savoir si les ordinateurs s'imposeront à l'avenir contre les humains lorsqu'il s'agira de vérifier des preuves mathématiques, Wojewodski et Felder répondent ouvertement. Wojewodski dit : "Nous ne sommes qu'au début d'une longue route de changement, et il est impossible de dire aujourd'hui où elle nous mènera". Felder dit : "Les ordinateurs peuvent faire des erreurs. Les humains peuvent faire des erreurs. Ce qui est s?r, c'est que les mathématiques deviendront plus complexes et que la démonstration ne sera pas plus facile".