Les mathématiques ont toujours reposé sur deux langages distincts. L'un est le langage naturel que nous utilisons pour expliquer des idées, raconter des histoires et partager des intuitions ; il est flexible, riche en contexte et omet souvent des étapes qui semblent évidentes pour un lecteur humain. L'autre est le langage formel des assistants de preuve, des systèmes informatiques rigides qui vérifient chaque mouvement logique pour s'assurer qu'une conclusion est indéniablement vraie. Pendant des décennies, des chercheurs ont travaillé à la traduction du premier langage vers le second, un processus appelé autoformalisation. L'objectif était simple : prendre une preuve écrite par un humain et la transformer en un code vérifiable par un ordinateur. Mais un problème critique persistait. Un ordinateur pouvait souvent produire une preuve techniquement correcte, mais qui ne ressemblait en rien à l'argument humain qui l'avait inspirée. L'ordinateur pouvait résoudre le problème en utilisant un chemin complètement différent, cachant le raisonnement original derrière un mur de raccourcis automatisés. Cela créait un fossé entre la vérité et la compréhension. Si la preuve de l'ordinateur ne suit pas les étapes de l'humain, nous ne pouvons pas l'utiliser pour vérifier si le raisonnement de l'humain était réellement sain, ni lui faire confiance pour nous enseigner comment l'argument fonctionne.

Une équipe de chercheurs a maintenant abordé ce fossé avec un nouveau système conçu pour que la preuve informatique reste fidèle au processus de pensée original de l'humain. Ils appellent leur système Pistis, un nom tiré du mot grec ancien pour la foi ou la confiance. Les chercheurs ont appliqué ce système aux trois premiers livres des Éléments d'Euclide, un texte fondateur de la géométrie écrit il y a plus de deux mille ans. Leur travail démontre qu'il est possible de traduire ces arguments anciens dans un langage informatique moderne sans perdre la logique originale, tout en mettant au jour des erreurs cachées dans le texte qui étaient passées inaperçues pendant des siècles.

Le défi central auquel l'équipe a été confrontée est que le langage naturel et la logique informatique opèrent selon des rythmes différents. Une preuve humaine peut dire : « Supposons que ceci soit vrai », et passer à la suite, attendant du lecteur qu'il comble le vide. Un ordinateur, cependant, exige que chaque étape soit explicitement énoncée et justifiée. Les tentatives précédentes de traduction de preuves laissaient souvent l'ordinateur combler ces lacunes avec sa propre logique, réécrivant de fait l'argument pour faciliter la tâche de la machine. Le résultat était une preuve qui compilait avec succès mais ne reflétait pas l'intention de l'auteur humain. Pistis a été construit pour empêcher cela. Au lieu de demander à l'ordinateur de trouver n'importe quel moyen de prouver l'énoncé, le système force l'ordinateur à suivre le chemin spécifique de l'humain, phrase par phrase.

Pour y parvenir, les chercheurs ont développé une méthode qui divise le processus de traduction en deux phases distinctes. Premièrement, une phase de cartographie analyse le texte en langage naturel et le divise en une séquence de petites étapes atomiques. Elle identifie exactement ce que chaque phrase affirme et les hypothèses sur lesquelles elle repose. Cela crée un modèle strict que l'ordinateur doit suivre. Deuxièmement, une phase de remplissage tente de prouver chacune de ces petites étapes individuellement. Le système utilise une stratégie de recherche spécialisée qui empêche l'ordinateur de prendre des raccourcis ou de devancer les étapes. Si l'ordinateur ne peut pas prouver une étape spécifique en utilisant les outils et les références exacts mentionnés dans le texte humain, il ne se contente pas de trouver un autre moyen de résoudre le problème. Au lieu de cela, il signale le problème, révélant que l'argument humain original pourrait comporter une faille ou une pièce manquante.

Cette approche s'est avérée remarquablement efficace lorsqu'elle a été testée sur la géométrie d'Euclide. Les chercheurs ont généré des preuves formelles pour 92 propositions à travers les trois premiers livres. Lorsqu'ils ont comparé ces nouvelles preuves aux tentatives précédentes, la différence était frappante. Les nouvelles preuves compilaient plus de trente-trois fois plus vite, une amélioration significative de l'efficacité qui suggère que la nouvelle méthode évite les calculs lourds et lents des anciens systèmes. Plus important encore, les experts humains qui ont examiné les preuves ont préféré le résultat du nouveau système par une large marge. Dans une étude en aveugle, les examinateurs ont trouvé les nouvelles preuves bien plus transparentes et de meilleures représentations des arguments du manuel original. Un juge doté d'intelligence artificielle, entraîné pour évaluer la qualité de la traduction, a également été d'accord, favorisant les nouvelles preuves par rapport aux anciennes selon un ratio de plus de cinq contre un.

Au-delà de la simple traduction du texte, le système a agi comme un vérificateur rigoureux exposant de véritables failles dans le matériel source. Parce que le système insiste pour suivre la logique humaine à la lettre, il ne peut pas cacher les erreurs. Dans un cas, le système a identifié une erreur de citation dans une traduction moderne d'Euclide. Le texte référençait une proposition sur la division d'une ligne en deux, mais la citation pointait vers une proposition sur la division d'un angle. Le système a signalé ce décalage, montrant que la traduction avait lié la mauvaise idée au mauvais pas. Dans un autre cas, le système a trouvé une lacune dans le raisonnement d'Euclide où un scénario spécifique n'était pas traité. Les chercheurs ont pu démontrer formellement que l'argument original était incomplet, une découverte qui aurait été difficile à faire sans un outil adhérant strictement à la structure originale.

Le succès de Pistis suggère que la formalisation fidèle n'est pas seulement un exercice technique, mais un outil puissant pour vérifier la connaissance humaine. En forçant l'ordinateur à suivre le même chemin que l'humain, le système peut confirmer si le raisonnement tient la route ou là où il se brise. Les chercheurs ont constaté que leur méthode pouvait accepter des arguments valides, réfuter des arguments invalides et localiser précisément l'endroit où une preuve a échoué. Cette capacité s'étend au-delà de la géométrie ancienne ; le cadre est conçu pour fonctionner avec n'importe quel argument mathématique écrit en langage naturel. Ce travail montre que nous n'avons pas à choisir entre la flexibilité de l'explication humaine et la rigueur de la vérification machine. Il est possible d'avoir les deux, à condition que la machine soit guidée pour respecter la voix et la logique originales de l'humain.

L'étude a également mis en évidence les limites de la technologie actuelle. Bien que le système ait bien fonctionné pour les trois premiers livres d'Euclide, il ne pouvait pas gérer chaque proposition des livres suivants sans une assistance humaine supplémentaire. Certaines propositions nécessitaient des concepts géométriques que le système informatique sous-jacent ne savait pas encore traiter, comme la mesure de la longueur d'une ligne courbe. Les chercheurs ont noté que leur système repose sur un humain ou une intelligence artificielle avancée pour agir comme un oracle, vérifiant que la cartographie initiale du texte est correcte. Cela signifie que le processus n'est pas encore totalement automatique, mais il réduit considérablement la charge de travail manuel par rapport aux méthodes précédentes.

En fin de compte, l'article présente une nouvelle norme pour notre interaction avec les preuves mathématiques à l'ère de l'intelligence artificielle. Il dépasse la question de savoir si un ordinateur peut prouver un théorème pour aborder la question plus profonde de savoir si l'ordinateur comprend l'argument. En garantissant que la preuve formelle reflète l'argument en langage naturel étape par étape, les chercheurs ont créé un outil capable de valider le raisonnement derrière une conclusion, et non seulement la conclusion elle-même. Cela permet aux mathématiciens et aux étudiants d'avoir la certitude que l'ordinateur ne se contente pas de trouver une solution, mais suit véritablement la logique de la personne qui a écrit la preuve. Ce travail offre une voie de passage où l'intuition humaine et la précision de la machine travaillent ensemble, préservant l'intégrité de la découverte mathématique tout en exploitant la puissance de la vérification moderne.