Une preuve controversée en mathématiques – qui divise le domaine depuis plus d’une décennie – pourrait finalement être tranchée par un juge improbable : un programme informatique. Le cœur du débat tourne autour de la tentative de Shinichi Mochizuki en 2012 de résoudre la conjecture ABC, un problème de longue date profondément enraciné dans la nature fondamentale des nombres.
La conjecture ABC se concentre sur une équation d’une simplicité trompeuse impliquant trois nombres entiers : a + b = c. Il pose des règles spécifiques régissant la relation entre les nombres premiers qui composent ces nombres entiers. Résoudre ce problème apparemment fondamental pourrait permettre de mieux comprendre les mathématiques, ce qui pourrait avoir un impact sur d’autres conjectures célèbres comme le dernier théorème de Fermat.
Mochizuki, professeur à l’Université de Kyoto au Japon, a présenté sa preuve dans un cadre complexe qu’il a inventé appelé théorie interuniverselle de Teichmüller (IUT). Cependant, la technicité et l’obscurité de la théorie de l’IUT la rendaient largement incompréhensible pour la plupart des mathématiciens tentant de vérifier son travail. L’enthousiasme initial a cédé la place à la frustration alors que les experts s’efforçaient d’en déchiffrer les subtilités.
Pour alimenter le feu, en 2018, deux éminents mathématiciens allemands, Peter Scholze et Jakob Stix, ont identifié une faille potentielle dans la preuve de Mochizuki. Mochizuki a contré leur argument, et sans un organisme global pour arbitrer les différends mathématiques, le domaine s’est divisé en deux camps : ceux qui acceptent largement le point de vue dominant (soutenu par la plupart des mathématiciens) et un groupe plus petit aligné sur Mochizuki et son institut de Kyoto.
Mochizuki propose désormais une voie à suivre grâce à la formalisation : en convertissant sa preuve d’une notation mathématique lisible par l’homme en Lean, un langage de programmation informatique spécialement conçu pour une vérification mathématique rigoureuse. Ce processus pourrait potentiellement permettre aux ordinateurs de vérifier automatiquement la cohérence de ses arguments, offrant ainsi un niveau d’objectivité sans précédent.
Mochizuki pense que Lean est particulièrement bien équipé pour surmonter les obstacles linguistiques et conceptuels complexes qui ont bloqué les progrès dans la compréhension de la théorie de l’IUT. Il le considère comme un outil permettant de libérer la vérité mathématique des biais potentiels inhérents à l’interprétation humaine.
Si certains experts comme Kevin Buzzard de l’Imperial College de Londres y voient une direction prometteuse, ils reconnaissent également le défi monumental qui nous attend. Formaliser la théorie de l’IUT nécessiterait de traduire de vastes pans d’équations complexes dans la syntaxe Lean – une entreprise semblable à certains des plus grands projets de formalisation jamais entrepris. De tels efforts impliquent souvent des équipes dédiées de mathématiciens et de programmeurs s’étalant sur des mois, voire des années.
Johan Commelin de l’Université d’Utrecht aux Pays-Bas, tout en étant prudemment optimiste, souligne que le succès dépend de l’engagement durable de Mochizuki. Il prévient que si le projet est abandonné prématurément, il pourrait simplement devenir un autre chapitre d’une longue saga marquée par des différends non résolus.
Même en cas de succès, Commelin souligne que même avec un code vérifié par ordinateur, des désaccords sur l’interprétation pourraient persister. Le Lean peut résoudre les contradictions logiques mais pas nécessairement apaiser toutes les différences philosophiques ou conceptuelles entourant le travail de Mochizuki.
En fin de compte, même si la formalisation offre une lueur d’espoir pour résoudre cette impasse mathématique persistante, il reste à voir si elle peut surmonter les complexités profondément enracinées et les perspectives divergentes qui ont caractérisé le débat sur la preuve de la conjecture ABC.
