Depuis plus d’une décennie, la communauté mathématique est engagée dans un débat acharné sur la validité d’une preuve massive et controversée. Aujourd’hui, une nouvelle frontière technologique – la formalisation assistée par ordinateur – offre un moyen potentiel de résoudre enfin le différend.
La controverse sur la conjecture ABC
Le conflit se concentre sur la conjecture ABC, un problème fondamental impliquant la relation entre l’addition et la multiplication dans les nombres premiers. En 2012, Shinichi Mochizuki de l’Université de Kyoto a publié une preuve de 500 pages prétendant résoudre cette énigme de longue date.
Cependant, sa méthode – un cadre complexe appelé théorie inter-universelle de Teichmüller (IUT) – était si sans précédent qu’elle a divisé la communauté mathématique mondiale. Alors que Mochizuki et ses partisans insistent sur le fait que la preuve est correcte, de nombreux mathématiciens éminents, dont Peter Scholze et Jakob Stix, soutiennent que la logique contient un défaut fatal.
Cette impasse a créé une « impasse » rare dans la science moderne : un côté voit une vérité révolutionnaire, tandis que l’autre voit un argument indéchiffrable ou brisé.
L’essor de la formalisation
Pour sortir de cette impasse, les chercheurs se tournent vers Lean, un langage de programmation spécialisé conçu pour la « formalisation ». Dans ce processus, les preuves mathématiques sont traduites en code qu’un ordinateur peut vérifier avec une certitude logique absolue. Cela supprime « l’élément humain » – le potentiel d’incompréhension, de pression sociale ou de biais d’évaluation par les pairs – et le remplace par une vérité binaire.
Deux projets distincts tentent actuellement d’utiliser cette technologie pour régler le problème :
1. Le projet LANA (La recherche de la vérité)
Dirigé par Kato Fumiharu au ZEN Mathematics Center, le projet de géométrie Lean et Anabelian (LANA) vise à vérifier la preuve une fois pour toutes. Ce groupe est composé d’experts des théories spécifiques de Mochizuki et du langage de programmation Lean.
Malgré leurs progrès, le projet se heurte à un obstacle important. Ils ont identifié un point spécifique et problématique dans la théorie de l’IUT qui fait écho à l’erreur identifiée par Scholze et Stix en 2018. Après dix-huit mois d’étude intensive, l’équipe reste bloquée sur ce nœud logique particulier.
2. Le projet de Mochizuki (La recherche de la clarté)
Dans une approche différente, Mochizuki et ses collègues ont également commencé à formaliser son travail en Lean. Cependant, leur objectif n’est pas de « prouver » leur propre exactitude – puisqu’ils pensent qu’elle est déjà établie – mais d’utiliser le code comme un outil de communication précis.
Mochizuki affirme que Lean créera un « enregistrement précis » de sa structure logique, la rendant ainsi à l’abri des interprétations erronées qui alimentent la controverse depuis des années. Bien que son équipe ait produit 70 lignes de code initiales, les experts notent que ce n’est que le tout début de ce qui sera probablement une tâche monumentale.
Pourquoi c’est important
La résolution de la conjecture ABC concerne plus qu’une simple équation ; cela représente un tournant dans la façon dont les mathématiques sont pratiquées.
- La crise de la validation : Si l’ordinateur détecte une erreur, cela réglera une décennie de frictions académiques.
- La nouvelle méthodologie : Si la preuve est vérifiée, elle prouve que la « formalisation » est un moyen viable de traiter des idées mathématiques de plus en plus complexes qui dépassent les limites cognitives humaines.
- The Communication Bridge : Le dialogue entre le projet LANA et le groupe de Mochizuki suggère que la technologie pourrait enfin fournir un langage commun aux mathématiciens qui, autrement, auraient été incapables de communiquer efficacement.
Conclusion
Même si les obstacles techniques restent immenses, le passage à des mathématiques vérifiées par ordinateur représente le premier véritable mouvement dans la controverse ABC depuis des années. Que le code confirme ou corrige le travail de Mochizuki, le résultat changera fondamentalement la manière dont la vérité mathématique est établie et communiquée.
