Depuis plus d’une décennie, les mathématiciens ne parviennent pas à s’entendre sur l’exactitude d’une preuve de 500 pages. Désormais, traduire la preuve sous une forme lisible par ordinateur pourrait enfin régler le problème.
Les ordinateurs peuvent vérifier les preuves mathématiques
L’un des débats les plus controversés en mathématiques pourrait être réglé à l’aide d’un ordinateur, mettant potentiellement fin à une âpre dispute sur une preuve complexe qui fait rage depuis plus d’une décennie.
Les problèmes ont commencé en 2012, lorsque Shinichi Mochizuki de l’Université de Kyoto au Japon a stupéfié le monde mathématique avec une preuve tentaculaire de 500 pages de la conjecture ABC, un problème important non résolu qui touche au cœur même de ce que sont les nombres. La preuve utilisait un cadre hautement technique et abstrus inventé par Mochizuki, appelé théorie inter-universelle de Teichmüller (IUT), qui semblait impénétrable même à la plupart des mathématiciens experts cherchant à la comprendre.
The ABC conjecture, which is now more than 40 years old, involves a seemingly simple equation of three whole integers, a + b = c, and dictates how the prime numbers that make up these numbers must relate to one another. En plus de donner un aperçu approfondi de la nature fondamentale de la manière dont l'addition et la multiplication interagissent, cette conjecture a des implications pour d'autres conjectures mathématiques célèbres, telles que le dernier théorème de Fermat.
Ces ramifications potentielles ont initialement enthousiasmé les mathématiciens quant à la vérification de la preuve, mais les premiers efforts ont échoué et Mochizuki a déploré que davantage d'efforts n'aient pas été faits pour digérer le travail. Puis, en 2018, deux éminents mathématiciens allemands, Peter Scholze de l'Université de Bonn et Jakob Stix de l'Université Goethe de Francfort, ont annoncé avoir localisé une possible faille dans la cuirasse de la preuve.
Mais Mochizuki a rejeté leur argument et, sans grand organe de jugement pour décider qui avait raison ou tort, la validité de la théorie de l'IUT s'est figée en deux camps : d'un côté, la plupart de la communauté mathématique ; de l'autre, un petit groupe de chercheurs vaguement affiliés à Mochizuki et à l'Institut de recherche en sciences mathématiques de Kyoto, où il est professeur.
Maintenant, Mochizuki a proposé une solution possible à cette impasse. Il a suggéré de traduire la preuve de sa forme actuelle, dans une notation mathématique conçue pour les humains, vers un langage de programmation appelé Lean, qui pourrait être automatiquement vérifié par un ordinateur.
Ce processus, appelé formalisation, est un domaine de recherche en cours qui pourrait complètement changer la manière dont les mathématiques sont élaborées. La formalisation de la preuve de Mochizuki a déjà été suggérée, mais c'est la première fois qu'il manifeste son désir d'aller de l'avant avec le projet.
Mochizuki n'a pas répondu à une demande de commentaires sur cet article, mais dans un rapport récent, il a soutenu que Lean serait bien adapté pour démêler les types de désaccords entre mathématiciens qui ont empêché l'acceptation généralisée de sa preuve : « (Lean) est la meilleure et peut-être la seule technologie… pour réaliser des progrès significatifs par rapport à l'objectif fondamental de libérer la vérité mathématique du joug des dynamiques sociales et politiques », écrit Mochizuki.
Selon Mochizuki, il a été convaincu des mérites de la formalisation après avoir assisté à une récente conférence sur le Lean à Tokyo en juillet, en particulier après avoir constaté sa capacité à gérer les types de structures mathématiques qu'il considère comme essentielles à sa théorie IUT.
Il s'agit d'une direction potentiellement prometteuse pour aider à sortir de l'impasse, estime Kevin Buzzard de l'Imperial College de Londres. « Si c'est écrit en Lean, alors ce n'est pas fou, n'est-ce pas ? Beaucoup de choses dans les journaux sont écrites dans un langage très étrange, mais si vous pouvez l'écrire en Lean, alors cela signifie qu'au moins ce langage étrange est devenu une chose complètement bien définie », dit-il.
« Nous voulons comprendre le pourquoi (de l'IUT), et nous l'attendons depuis plus de 10 ans », déclare Johan Commelin de l'Université d'Utrecht aux Pays-Bas. « Lean pourrait nous aider à comprendre ces réponses. »
Cependant, Buzzard et Commelin affirment que formaliser la théorie de l’IUT serait une entreprise gigantesque et impliquerait de traduire des quantités d’équations mathématiques qui n’existent actuellement que sous une forme lisible par l’homme. Ce projet serait à la hauteur de certains des plus grands efforts de formalisation jamais réalisés, qui impliquent souvent des équipes de mathématiciens experts et de programmeurs Lean, prenant des mois ou des années.
Cette perspective intimidante pourrait s’avérer peu attrayante pour la petite poignée de mathématiciens qualifiés pour entreprendre le projet. « Les gens vont devoir faire un grand choix pour savoir s'ils veulent consacrer une grande partie de leur temps à travailler sur un projet qui pourrait finalement s'avérer être un échec », explique Buzzard.
Mais même si les mathématiciens parviennent à mener à bien le projet et que le code Lean montre que le théorème de Mochizuki n'a pas de contradictions, les mathématiciens, y compris Mochizuki lui-même, pourraient encore se battre sur sa signification, explique Commelin.
« Le Lean peut avoir beaucoup d'impact et mettre un terme à la controverse, mais seulement si Mochizuki s'en tient vraiment à sa nouvelle résolution de formaliser son travail », dit-il. « S'il s'en va après quatre mois en disant : 'D'accord, j'ai essayé, mais Lean est tout simplement trop stupide pour comprendre ma preuve', alors ce n'est qu'un nouveau chapitre dans une très longue série de chapitres où nous sommes toujours coincés avec un problème social. »
Et, malgré tout l'optimisme dont Mochizuki fait preuve à l'égard du Lean, il est également d'accord avec ses critiques sur le fait que l'interprétation du sens du code pourrait conduire à de nouveaux désaccords, écrivant que Lean « ne semble pas à l'heure actuelle constituer une sorte de « remède magique » pour la résolution complète des problèmes sociaux et politiques.
Cependant, Buzzard espère qu’une formalisation réussie pourrait, au moins, faire avancer la saga qui dure depuis une décennie, surtout si Mochizuki réussit. « Vous ne pouvez pas contester le logiciel », dit-il.
