Un différend de dix ans en mathématiques concernant la preuve de la conjecture ABC par Shinichi Mochizuki pourrait être résolu par une formalisation informatique. Mochizuki a suggéré de traduire son œuvre de 500 pages dans le langage de programmation Lean pour une vérification automatisée. Cette approche pourrait combler les divisions entre les camps rivaux de la communauté mathématique.
La controverse remonte à 2012, lorsque Shinichi Mochizuki, professeur à l'Université de Kyoto au Japon, a publié une preuve volumineuse de 500 pages pour la conjecture ABC. Ce problème vieux de 40 ans concerne l'équation a + b = c pour les entiers complets et les relations entre leurs facteurs premiers, avec des implications pour des théorèmes comme le dernier théorème de Fermat. La preuve de Mochizuki repose sur sa théorie complexe de Teichmüller inter-universelle (IUT), que de nombreux experts ont trouvée difficile à appréhender.
L'enthousiasme initial s'est estompé alors que les efforts de vérification se sont enlisés. En 2018, Peter Scholze de l'Université de Bonn et Jakob Stix de l'Université Goethe de Francfort ont identifié une faille potentielle, contestée par Mochizuki. Sans autorité centrale, le monde mathématique s'est divisé : la plupart des mathématiciens d'un côté, et un groupe plus restreint affilié à Mochizuki et à l'Institut de recherche en sciences mathématiques de Kyoto de l'autre.
Pour briser l'impasse, Mochizuki prône désormais la formalisation de la preuve en Lean, un langage pour les mathématiques vérifiées par ordinateur. Inspiré par une conférence de juillet à Tokyo, il argue dans un rapport récent que Lean pourrait libérer la vérité mathématique des "dynamiques sociales et politiques". Comme il l'écrit : « [Lean] est la meilleure et peut-être la seule technologie… pour obtenir un progrès significatif en vue de l'objectif fondamental de libérer la vérité mathématique du joug des dynamiques sociales et politiques. »
Les experts y voient du potentiel mais restent prudents. Kevin Buzzard du Imperial College London note : « Si c'est écrit en Lean, ce n'est pas de la folie, n'est-ce pas ? Beaucoup de choses dans les articles sont écrites dans un langage très étrange, mais si on peut les écrire en Lean, cela signifie au moins que ce langage étrange est devenu une chose complètement bien définie. » Johan Commelin de l'Université d'Utrecht ajoute : « Nous voulons comprendre le pourquoi [de l'IUT], et nous attendons cela depuis plus de 10 ans. Lean pourrait nous aider à comprendre ces réponses. »
Cependant, la tâche est immense, nécessitant des équipes de spécialistes et potentiellement des années de travail. Même en cas de succès, cela pourrait ne pas mettre fin aux débats sur l'interprétation, comme Mochizuki le reconnaît : Lean n'offre pas de « remède miracle » aux problèmes sociaux. Buzzard reste optimiste : « On ne peut pas discuter avec le logiciel. »