🤖 AI

Case study: proving sqrt(2) irrational with LPTP and an LLM

Cet article présente une étude de cas démontrant comment un LLM, guidé par des définitions de programmation logique de base et vérifié par le prouveur de théorèmes LPTP, peut générer avec succès une preuve formelle complète et lisible par l'humain de l'irrationalité de la racine carrée de 2.

Auteurs originaux : Fred Mesnard, Étienne Payet, Wim Vanhoof

Publié 2026-07-24

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Fred Mesnard, Étienne Payet, Wim Vanhoof

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous êtes un détective tentant de résoudre un mystère qui intrigue les humains depuis plus de deux mille ans : la racine carrée de 2 est-elle un nombre « rationnel » ? Dans le monde des mathématiques, un nombre rationnel est comme une fraction parfaite, une part de tarte bien nette (comme 3/4 ou 5/2). Un nombre irrationnel est un nombre décimal désordonné et infini qui ne peut jamais s'écrire sous la forme d'une fraction simple. La racine carrée de 2 est la longueur de la diagonale d'un carré dont les côtés mesurent 1, et les mathématiciens anciens ont prouvé qu'elle est désordonnée — elle ne peut pas être une fraction.

Maintenant, imaginez que vous disposez de deux outils très différents pour vous aider à résoudre ce mystère. Le premier est un arbitre robotique très strict appelé LPTP. Il parle un langage très précis et logique (basé sur Prolog) et n'acceptera une preuve que si chaque étape est mathématiquement parfaite. Si vous faites ne serait-ce qu'une minuscule erreur, il frappera son marteau et dira : « Non, invalide. » Le second outil est un Modèle de Langage Étendu (LLM), qui est comme un étudiant super intelligent et créatif ayant lu presque tout ce qui a été écrit. Cet étudiant est excellent pour deviner l'étape suivante d'une histoire ou d'un problème mathématique, mais il peut parfois « halluciner », en inventant des faits qui semblent corrects mais qui sont en réalité faux.

La grande question pour les scientifiques aujourd'hui est la suivante : pouvons-nous unir ces deux outils ? Pouvons-nous laisser l'étudiant créatif faire le gros du travail de rédaction, pendant que le arbitre strict vérifie chaque phrase pour s'assurer que l'étudiant ne ment pas ? Ce document explore précisément ce partenariat, en utilisant le mystère ancien de la racine carrée de 2 comme cas de test.

Le Grand Partenariat de Vérification de Preuves

Dans cet article, les auteurs ont entrepris de voir s'ils pouvaient utiliser une IA moderne (spécifiquement un modèle appelé Claude) pour aider à prouver que la racine carrée de 2 est irrationnelle, mais avec une nuance : la preuve devait être écrite dans un format très spécifique et strict que l'arbitre robotique (LPTP) pourrait comprendre et vérifier. Ils ne voulaient pas seulement que l'IA dise « c'est vrai » ; ils voulaient que l'IA rédige la logique étape par étape, que l'arbitre noterait ensuite.

L'histoire commence par une idée simple. Pour prouver que la racine carrée de 2 est irrationnelle, on suppose généralement le contraire : qu'elle est une fraction composée de deux nombres entiers, $p$ et $q$ , qui ne partagent aucun facteur commun (ils sont « premiers entre eux »). Si l'on fait les calculs, on finit par tomber sur une contradiction où les deux nombres doivent être pairs, ce qui signifie qu'ils partagent effectivement un facteur (2). Cela brise la règle selon laquelle ils étaient premiers entre eux, prouvant ainsi que l'hypothèse initiale était fausse.

Les auteurs ont tenté d'amener l'IA à écrire cette preuve dans le langage strict de LPTP. Au début, l'IA était comme un étudiant qui connaît l'histoire mais ne parvient pas à rédiger la dissertation dans le format requis. Elle tentait de sauter des étapes ou de faire des bonds logiques que l'arbitre n'accepterait pas.

C'est ici que le travail d'équipe a eu lieu. Les auteurs ont mis en place une boucle de rétroaction :

L'IA tente de rédiger une étape de la preuve.
L'arbitre (LPment LPTP) vérifie cette étape.
Si l'arbitre trouve une erreur, il indique la ligne exacte où la logique a échoué.
Les auteurs présentent cette erreur à l'IA.
L'IA essaie à nouveau, en corrigeant l'erreur spécifique.

Ce processus ressemblait à un jeu de « chaud et froid ». L'arbitre ne se contentait pas de dire « faux » ; il disait : « Vous avez fait une erreur à l'étape 4 », permettant à l'IA de corriger sa trajectoire.

Les Résultats : Une Victoire Partielle

L'expérience a été un succès, mais avec quelques nuances. L'IA a été capable de prouver de nombreuses parties plus petites et plus faciles du puzzle par elle-même. Par exemple, elle a prouvé avec succès que « si un nombre est pair, son carré est pair » ou que « 2 fois un nombre est pair ». Les auteurs appellent cela des « lemmes » (petites preuves auxiliaires). L'IA a réussi ces étapes, allant même parfois jusqu'à proposer de nouvelles idées d'aide que les humains n'avaient pas envisagées.

Cependant, pour la partie la plus complexe de la preuve — la logique spécifique montrant pourquoi la racine carrée de 2 ne peut pas être une fraction — l'IA est restée bloquée. Elle n'a pas réussi à trouver le bon chemin par elle-même. Ainsi, les auteurs humains ont dû intervenir pour donner un « indice » ou même écrire la structure principale de la preuve eux-mêmes, en demandant à l'IA de combler les lacunes plus petites.

Finalement, ils ont produit une preuve formelle complète démontrant que la racine carrée de 2 est irrationnelle. Cette preuve a été partiellement rédigée par l'IA et entièrement vérifiée par le robot arbitre. L'arbitre lui a donné une note de passage, confirmant que la logique était solide.

Ce que cela signifie

L'article ne prétend pas que l'IA peut désormais résoudre tous les problèmes mathématiques de manière autonome. En fait, les auteurs montrent explicitement que l'IA ne peut pas le faire seule ; sans la guidance humaine et la vérification stricte de l'arbitre, l'IA aurait probablement produit une preuve fausse ou erronée.

Au lieu de cela, l'article suggère une nouvelle façon de travailler : l'IA comme rédactrice de brouillons, les humains comme éditeurs, et les outils formels comme vérificateurs de faits. L'IA est rapide et créative, générant des idées et remplissant les détails, tandis que l'outil formel (LPTP) agit comme un œil implacable qui détecte les hallucinations et les erreurs.

Les auteurs ont également testé d'autres outils mathématiques automatisés (appelés ATP) pour voir s'ils pouvaient accomplir la tâche plus rapidement. Ces outils étaient rapides et gratuits, mais ils produisaient des preuves difficiles à lire pour les humains et qui ne pouvaient pas être facilement ajoutées à la bibliothèque de mathématiques vérifiées. L'approche par l'IA, bien que plus lente et nécessitant l'aide humaine, produisait des preuves lisibles et pouvant être stockées en toute sécurité pour un usage futur.

En résumé, cet article montre que nous n'avons pas besoin de choisir entre l'intuition humaine et la précision de la machine. En laissant l'IA effectuer le gros du travail de rédaction et les outils stricts assurer la notation, nous pouvons construire un système où l'IA nous aide à prouver des vérités mathématiques complexes, tant que nous gardons un humain pour diriger le navire et un arbitre strict pour vérifier la carte. La racine carrée de 2 est toujours irrationnelle, mais nous disposons désormais d'une nouvelle méthode collaborative pour le prouver.

Résumé Technique : Étude de cas prouvant l'irrationalité de $\sqrt{2}$ avec LPTP et un LLM

Énoncé du Problème
Le document traite du défi que représente la preuve formelle de l'irrationalité de la racine carrée de 2 dans le contexte de la programmation logique (LP). Plus précisément, les auteurs visent à prouver qu'il n'existe pas deux nombres entiers naturels premiers entre eux, $p$ et $q$ , tels que $p^2 = 2q^2$ . Bien qu'il s'agisse d'un résultat mathématique classique, les moteurs de programmation logique standard basés sur la résolution (comme Prolog) ne peuvent pas fournir de réponse négative à la requête correspondante car l'espace de recherche sur les entiers naturels est infini. Les auteurs cherchent à combler cette lacune en utilisant le système LPTP (Logic Program Theorem Prover) pour générer une preuve formelle et en évaluant dans quelle mesure un grand modèle de langage (LLM) peut aider à la construction de cette preuve.

Méthodologie
Les auteurs emploient une approche hybride combinant le système de vérification formelle LPTP avec un LLM (spécifiquement Claude Opus 4.5 d'Anthropic).

Cadre Formel (LPTP) :
- LPTP est utilisé pour vérifier les propriétés de programmes logiques basés sur la logique du premier ordre et la complétion de Clark.
- Le système distingue le succès, l'échec et la terminaison des prédicats en utilisant des opérateurs spécifiques ( $S$ , $F$ , $T$ ) et prend en charge les schémas d'induction pour les prédicats récursifs.
- Le langage de preuve est basé sur la déduction naturelle, garantissant la lisibilité pour l'humain.
- Les auteurs définissent le problème à l'aide de prédicats Prolog purs pour les nombres naturels (arithmétique de Peano), l'addition, la multiplication et le PGCD.
Stratégie d'Intégration du LLM :
- Apprentissage en Contexte (In-Context Learning) : Le LLM reçoit le manuel de l'utilisateur de LPTP (PDF) ainsi que deux bibliothèques de base (nombres de Peano et listes) contenant du code Prolog et des preuves existantes.
- Boucle de Rétroaction Itérative : Les auteurs soumettent des lemmes au LLM en syntaxe LPTP (ou en langage naturel). Le LLM génère une tentative de preuve, qui est immédiatement injectée dans le vérificateur de preuve LPTP.
- Correction d'Erreurs : Si le vérificateur LPTP rejette la preuve, il signale la première étape de dérivation incorrecte. Cette erreur spécifique est renvoyée au LLM pour affiner la preuve.
- Supervision Humaine : Un développateur humain gère l'ordre des lemmes, décide quand abandonner des boucles improductives et fournit des indices de haut niveau ou la structure de la preuve pour les étapes difficiles.
Outils Auxiliaires :
- Les auteurs ont également utilisé des prouveurs de théorèmes automatiques (ATP) de premier ordre (FOL) prêts à l'emploi comme Vampire et E en traduisant les axiomes LPTP en syntaxe FOF. Ces outils ont été utilisés pour vérifier les lemmes de manière indépendante, bien que leurs preuves par résolution ne puissent pas être directement intégrées dans le cadre de déduction naturelle de LPTP.

Contributions Clés et Résultats

Construction de Preuve : L'équipe a réussi à construire une preuve complète et vérifiée par machine de l'irrationalité de $\sqrt{2}$ dans LPTP. La preuve a été partiellement générée par le LLM et entièrement validée par le vérificateur LPTP.
Génération de Lemmes :
- Le LLM a réussi à prouver plusieurs lemmes auxiliaires directement (par exemple, $2^2=4$ , propriétés des nombres pairs/impairs) ou après quelques itérations de correction d'erreurs (par exemple, des lemmes de simplification).
- Pour le lemme le plus complexe, evenpp:evenp (prouver que si le carré d'un nombre est pair, le nombre lui-même est pair), le LLM a initialement échoué. Les auteurs ont fourni un indice en langage naturel décrivant la preuve par cas (pair vs impair), après quoi le LLM a généré avec succès la preuve formelle.
- Le théorème principal (sqrt2:irrational) nécessitait que les auteurs fournissent le squelette de la preuve ; le LLM a ensuite rempli les étapes nécessaires et les lemmes auxiliaires.
Comparaison avec les ATP : Bien que les ATP aient pu prouver 9 des 12 lemmes dans la version finale, ils ont échoué à prouver le théorème principal dans le délai de 20 secondes, probablement en raison de l'expansion de l'espace de recherche. Crucialement, les preuves des ATP ne pouvaient pas être directement converties en preuves de déduction naturelle requises par LPTP.
Gestion des Dépendances : Le document détaille le graphe de dépendance des lemmes, montrant comment la capacité du LLM à prouver des propriétés simples (comme nat:natsquare ou sqr2:4) était essentielle pour prouver des propriétés de niveau supérieur.

Signification et Revendications
Les auteurs affirment que ce travail représente l'une des premières interactions entre LPTP et un LLM. Leur contribution principale est de démontrer un flux de travail semi-automatisé où :

Le Vérificateur de Preuve est Central : Le vérificateur LPTP agit comme le filtre critique contre les hallucinations du LLM. Il fournit un retour précis (la première étape incorrecte), permettant au LLM de s'autocorriger efficacement.
Rôles Complémentaires : Les ATP sont rapides et locaux mais produisent des preuves dans un format (résolution/superposition) incompatible avec la déduction naturelle de LPTP. Les LLM, guidés par le vérificateur, peuvent générer des preuves dans le bon format, bien qu'ils nécessitent une guidance humaine pour les étapes structurelles complexes.
Faisabilité pour la Programmation Logique (LP) : L'étude valide que les LLM peuvent être efficacement intégrés dans la vérification des propriétés de la programmation logique, à condition qu'une boucle de vérification de preuve rigoureuse soit en place.

L'article conclut modestement, notant que bien que le LLM n'ait pas pu générer l'intégralité de la structure de la preuve de manière autonome pour le théorème principal, il a réussi à gérer les étapes logiques granulaires une fois la structure définie. Cela ouvre la voie à de futures approches assistées par l'IA pour prouver les propriétés de Prolog, les auteurs prévoyant d'évaluer cette combinaison sur un ensemble plus large de problèmes de vérification.

Le Grand Partenariat de Vérification de Preuves

Les Résultats : Une Victoire Partielle

Ce que cela signifie

Articles similaires