💻 computer science

Auto formalisation of Chaitin and of the surprise incompleteness Theorem

Cet article présente une étude de cas utilisant un LLM (Claude) pour autoformaliser la preuve de Chaitin du premier théorème d'incomplétude et la version de Kritchman-Raz du paradoxe de l'examen surprise du second théorème d'incomplétude en Agda, démontrant la capacité du modèle à construire des simulations computationnelles complexes et à produire des preuves vérifiées par machine tout en mettant en évidence les forces et les limites actuelles du raisonnement mathématique.

Auteurs originaux : Thierry Coquand

Publié 2026-06-12

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Thierry Coquand

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

La vue d'ensemble : Enseigner les mathématiques à un robot

Imaginez que vous avez un robot très intelligent (une IA nommée Claude) et un manuel de mathématiques très strict et régi par des règles appelé « Basic Recursive Arithmetic ». Ce manuel est comme un jeu avec des règles très spécifiques : vous ne pouvez utiliser que le comptage de base et une logique simple, sans raccourcis sophistiqués ou « tours de magie ».

L'objectif de ce papier est de voir si le robot peut lire une preuve mathématique célèbre et complexe (sur la raison pour laquelle les mathématiques ont des limites) et la réécrire entièrement dans le langage strict de ce manuel, sans qu'un humain n'écrive une seule ligne de code.

La réponse est oui. Le robot a réussi à traduire deux idées mathématiques profondes dans ce langage strict, créant une preuve qu'un ordinateur peut vérifier comme étant 100 % correcte.

Les deux idées principales

Le papier se concentre sur deux concepts célèbres : la Preuve de Chaitin (liée au premier théorème d'incomplétude) et le Paradoxe de l'examen surprise (une version du second théorème d'incomplétude).

1. Le jeu de la « description courte » (La preuve de Chaitin)

Imaginez que vous avez une bibliothèque contenant toutes les histoires possibles que vous pourriez écrire en utilisant un ensemble limité de lettres.

La règle : Certaines histoires sont très courtes et faciles à décrire. D'autres sont si complexes que la façon la plus courte de les décrire est simplement d'écrire toute l'histoire.
Le problème : La preuve de Chaitin tente de trouver une histoire qui est si complexe qu'elle ne peut pas être décrite par un programme court.
Le défi du robot : Pour prouver cela, le robot a dû construire une « machine » à l'intérieur du manuel de mathématiques capable de lire une histoire, de l'exécuter et de voir ce qu'elle fait.
L'obstacle : Le manuel de mathématiques est trop simple pour gérer naturellement « l'exécution d'un programme », car cela nécessite généralement une fonction complexe (comme la fonction d'Ackermann) que le manuel ne permet pas.
La solution : L'auteur humain a suggéré une astuce appelée « majoration de Gandy/Howard ». Considérez cela comme le fait de donner au robot un réservoir de carburant. Au lieu de demander à la machine de s'exécuter indéfiniment, le robot calcule exactement la quantité de « carburant » (étapes) dont un programme a besoin pour se terminer. Il construit une jauge de carburant spéciale qui garantit que le programme s'arrêtera avant que le réservoir ne soit vide.
Le résultat : Le robot a construit cette jauge de carburant de lui-même. Il a prouvé que si vous essayez de décrire un nombre qui est « trop complexe pour être décrit simplement », vous créez une contradiction logique (comme prouver que 0 est égal à 1).

2. L'« examen surprise » et le tas de sable

La deuxième partie du papier traite d'un paradoxe célèbre : Un professeur annonce qu'il y aura un examen surprise la semaine prochaine. Les étudiants raisonnent en disant que ce ne peut pas être vendredi (car s'ils n'ont pas eu l'examen d'ici jeudi, ils sauront que c'est vendredi), donc ce ne peut pas être jeudi, et ainsi de suite... jusqu'à ce qu'ils conclent qu'il ne peut y avoir aucun examen du tout. Mais ensuite, le professeur le donne le mercredi, et c'est une surprise.

Le papier utilise une version de ce raisonnement (par Kritchman et Raz) pour prouver qu'un système mathématique ne peut pas prouver sa propre cohérence (qu'il ne contient pas de contradictions).

L'ancienne méthode : Les preuves précédentes comptaient le nombre de jours ou de nombres pour trouver une contradiction.
La nouvelle méthode (Le Sorite/Le tas de sable) : Les auteurs comparent cela au paradoxe du tas de sable.
- Si vous avez un tas de sable et que vous en retirez un grain, c'est toujours un tas.
- Si vous en retirez un autre, c'est toujours un tas.
- Si vous continuez à retirer les grains un par un, vous finirez par avoir zéro grain. Mais à quel moment exact a-t-il cessé d'être un « tas » ?
L'application :
- Imaginez une liste de nombres de 0 à un très grand nombre $N$ .
- La logique tente de prouver : « Il est impossible que tous ces nombres aient une description courte. »
- Le robot prouve cela étape par étape. Il dit : « Si nous supposons que les nombres de 0 à $N$ ont tous des descriptions courtes, nous obtenons une contradiction. »
- Puis il retire 0. « D'accord, si les nombres de 1 à $N$ ont des descriptions courtes, nous obtenons toujours une contradiction. »
- Il continue de retirer un nombre à la fois (comme on retire des grains de sable).
- Finalement, il atteint un point où la liste est vide, mais la logique impose quand même une contradiction.
Le rebondissement : Le papier soutient qu'il ne s'agit pas d'un « cercle vicieux » d'auto-référence ; c'est plutôt comme le tas de sable. Vous pouvez retirer un grain (un nombre) en toute sécurité, mais si vous continuez ainsi, toute la structure s'effondre. Cet effondrement prouve que le système mathématique ne peut pas prouver qu'il est sûr (cohérent) sans se briser lui-même.

Pourquoi cela importe (selon le papier)

L'IA comme assistant mathématique : Le papier montre que l'IA actuelle (comme Claude) est désormais capable de gérer les détails minuscules et fastidieux des preuves mathématiques complexes. Elle peut construire des parseurs, évaluer des machines et gérer des étapes logiques que les humains doivent habituellement faire manuellement.
Mathématiques constructives : Le papier souligne que dans les « mathématiques constructives » (où l'on doit réellement construire la chose dont on parle), l'idée d'une « fonction partielle » (un programme qui pourrait tourner indéfiniment) est délicate. Le robot a dû utiliser un programme « en boucle » qui pourrait tourner indéfiniment, mais la preuve garantit qu'il s'arrêtera. C'est une distinction subtile mais cruciale que l'IA a gérée correctement.
Pas de tours de magie : Le robot n'a pas utilisé de « tactiques » (raccourcis) ou de bibliothèques sophistiquées. Il a tout construit à partir de zéro en utilisant uniquement les règles de base du système mathématique. Cela rend la preuve très robuste et facile à vérifier par un ordinateur.

La conclusion

Ce papier est une étude de cas montrant que l'IA peut désormais agir comme un partenaire puissant dans les mathématiques formelles. Elle peut prendre une idée de haut niveau (comme « les mathématiques ont des limites ») et la traduire dans un format rigide, vérifiable par une machine.

Les auteurs notent que, bien que l'IA ait besoin d'un humain pour la guider (comme suggérer l'astuce du « réservoir de carburant »), l'IA peut ensuite écrire le code de manière autonome, construire la logique et documenter l'ensemble du processus. Le résultat est une preuve entièrement vérifiée qui clarifie exactement comment ces paradoxes logiques profonds fonctionnent, en éliminant l'ambiguïté pour ne laisser que les faits logiques bruts.

Résumé Technique : Auto-formalisation de Chaitin et du Théorème de l'Incomplétude de la Surprise

Problème et Contexte
Ce rapport étend une expérience précédente d'auto-formalisation du second théorème d'incomplétude de Gödel en utilisant le grand modèle de langage (LLM) Claude et l'assistant de preuve Agda. L'objectif principal est d'étudier les capacités et les limites des LLM actuels à formaliser des preuves mathématiques complexes, spécifiquement celles impliquant la représentation interne du calcul. Le document se concentre sur deux cibles spécifiques : la preuve de Chaitin du premier théorème d'incomplétude et la version du second théorème d'incomplétude de Kritchman-Raz, dite du « paradoxe de l'examen de surprise ».

Un défi technique central abordé est l'encodage du calcul au sein de l'Arithmétique Récursive Basique (BRA), un système (formulé par Guard) qui ne possède ni quantificateurs d'objets ni tactiques standards. Dans un tel système, définir une fonction d'évaluation interne est impossible car cela dépasserait les limites de la récursivité primitive (similaire à la fonction d'Ackermann). Le problème nécessite de représenter les programmes et leurs étapes d'exécution entièrement dans le langage objet, sans dépendre de fonctions méta-théoriques ou de bibliothèques externes.

Méthodologie
Le projet emploie une approche « spartiate » où aucune ligne de code Agda n'a été écrite par l'auteur humain ; la formalisation a été générée de manière autonome par Claude à partir de descriptions mathématiques de haut niveau. La méthodologie repose sur les stratégies techniques suivantes :

Encodage par chaînes ternaires : Les programmes sont représentés comme des nombres naturels interprétés comme des chaînes ternaires (chiffres 1, 2, 3). Cela permet de traiter l'ensemble des programmes de longueur au plus $L^*$ comme un simple segment initial de nombres naturels $\{p < N\}$ , où $N = 3^{L^*+1}$ , évitant ainsi des mécanismes d'énumération complexes.
Implémentation de la machine CK : Pour contourner la nécessité d'une fonction d'évaluation globale, Claude a construit de manière autonome une machine d'évaluation pas-à-pas par pile de continuations (une machine CK de Landin). Cette machine décompose les expressions et gère une pile de continuations, permettant de simuler le calcul étape par étape.
Majoration de Gandy/Howard : Un obstacle critique a été de prouver que la machine s'arrête dans un nombre spécifique d'étapes pour une fonction $f$ donnée à l'intérieur de la logique. Puisque le nombre d'étapes ne peut pas être un entier méta-théorique, les auteurs ont guidé Claude pour utiliser la méthode de majoration de Gandy/Howard. Cela consiste à définir un combinateur fermé fuel(f) via la récursion primitive qui majore de manière prouvable le temps d'exécution réel de $f$ . Cela permet d'énoncer et de prouver la complétude de l'interprète de manière interne dans BRA.
La Surprise comme Sorite : La preuve du second théorème d'incomplétude évite les arguments de comptage utilisés par Kritchman et Raz. Au lieu de cela, elle modélise l'argument comme un paradoxe du Sorite (un tas de sable). Elle procède par induction externe sur une étape $r$ , prouvant qu'il est impossible que tous les nombres dans l'intervalle $[r, N]$ possèdent des descriptions courtes.

Contributions Clés et Résultats
Le document présente une preuve entièrement vérifiée par machine dans Agda des résultats suivants pour l'Arithmétique Récursive Basique de Church :

Théorème de Chaitin auto-formalisé : Le système a réussi à formaliser la preuve de Chaitin, qui remplace la phrase du menteur par la complexité de Kolmogorov. La formalisation produit un transformateur de preuve explicite $G$ . Le théorème stipule que si un terme $w$ code une preuve de l'énoncé d'incompressibilité $K(out(w)) > L^*$ , alors $G \cdot w$ code une preuve de $0=1$ . Ceci est formulé comme une implication positive au niveau de l'objet plutôt que comme une négation méta-théorique de la prouvabilité.
Second Incomplétude Internalisé : Le document formalise l'argument de Kritchman-Raz pour montrer que si $T$ prouve sa propre cohérence ( $Con_T$ ), alors $T$ est incohérente ( $0=1$ ). La preuve procède par une descente de $S(0)$ (le principe du tiroir) vers $S(N+1)$ (une contradiction), où chaque étape $S(r) \to S(r+1)$ consomme l'hypothèse de cohérence exactement une fois.
Perspectives Constructives : La formalisation met en lumière le rôle des fonctions partielles dans les mathématiques constructives. Plus précisément, le programme diagonalise énumère les formules dérivables jusqu'à ce qu'une cible soit trouvée. Bien que le programme soit prouvé comme terminant de l'extérieur, sa taille est calculée sans internaliser la preuve de terminaison. Cela démontre une manifestation du phénomène de l'accélération de Blum (speed-up), où le fait de permettre un programme récursif partiel (maintenu total par une preuve externe) permet des programmes sans limite de plus en plus courts par rapport à ceux qui doivent certifier leur terminaison en interne.

Signification et Revendications
Le document affirme que les LLM de codage actuels, tels que Claude, sont des outils efficaces pour comprendre les détails granulaires des articles mathématiques, à condition qu'ils opèrent sous une supervision constante. Le projet sert d'étude de cas démontrant que :

Les LLM peuvent générer de manière autonome des mécanismes syntaxiques complexes (analyseurs, machines d'évaluation) et des arguments logiques (majoration) lorsqu'ils sont guidés par des indices structurels de haut niveau.
La théorie des types (spécifiquement Agda sans tactiques) est bien adaptée pour exprimer des mathématiques concrètes impliquant le calcul et le codage, car les preuves peuvent être représentées directement sans avoir besoin d'extensionalité de fonction ou de types quotients.
L'argument de la « surprise », lorsqu'il est formalisé, s'aligne plus étroitement sur le paradoxe du Sorite que sur le traditionnel paradoxe de l'examen de surprise, car la contradiction provient de l'itération d'étapes valides plutôt que d'une boucle auto-référentielle unique.

Les auteurs concluent que si le langage de la théorie des types est parfait pour ces mathématiques combinatoires et computationnelles, une question de recherche clé demeure : comment concevoir des systèmes formels capables de gérer des objets non combinatoires avec une automatisation similaire. La formalisation clarifie les détails implicites des présentations originales de Chaitin et Kritchman-Raz et fournit un fondement rigoureux, vérifié par machine, pour ces arguments au sein d'un cadre arithmétique minimal.