Proof by Mechanization: Cubic Diophantine Equation Satisfiability is $Σ^0_1$-Complete

Les auteurs démontrent que la satisfiabilité d'une unique équation diophantienne de degré total inférieur ou égal à 3 sur les entiers naturels est $\Sigma^0_1$-complète et donc indécidable, en établissant une correspondance mécanique vérifiée par Rocq entre la prouvabilité dans $\mathrm{I}\Delta_0+\mathrm{B}\Sigma_1$ et la solvabilité d'un système contraint réduit à un seul polynôme universel cubique.

L'essentiel

🧩 Le Grand Défi : Trouver la Solution Ultime en 3D

Imaginez que vous êtes un détective mathématique. Votre mission est de résoudre une énigme : existe-t-il une solution pour une équation donnée ?

Dans le monde des mathématiques, il existe des équations très simples (linéaires, comme $x + 2 = 5$) que n'importe qui peut résoudre. Il y a aussi des équations un peu plus complexes (quadratiques, comme $x^2 + y^2 = 25$) qui sont gérables. Mais dès qu'on monte d'un cran en complexité, le chaos s'installe.

Ce papier, écrit par Milan Rosko, raconte l'histoire de la découverte d'un seuil critique. Il prouve que dès qu'une équation atteint un certain niveau de complexité (appelé "degré 3" ou cubique), il devient impossible de créer un algorithme universel capable de dire "oui" ou "non" pour toutes les équations de ce type. C'est ce qu'on appelle l'indécidabilité.

Voici comment l'auteur y arrive, étape par étape, avec des images simples.

---

1. Le Contexte : La Machine à Preuves

Imaginez un système informatique très basique, un peu comme un vieux calculateur qui ne sait faire que de l'addition et compter. C'est ce que l'auteur appelle l'Arithmétique des Registres (RA).

• L'objectif : Vérifier si une preuve mathématique est valide.
• Le problème : Comment transformer la vérification d'une preuve (une suite logique de phrases) en une simple équation mathématique ?

L'auteur a construit un traducteur automatique (un compilateur). Ce traducteur prend une preuve mathématique et la transforme en une équation.

• Si la preuve est valide ➔ L'équation a une solution.
• Si la preuve est fausse ➔ L'équation n'a aucune solution.

2. Le Secret : Pourquoi le "Degré 3" est la clé ?

Pour comprendre le génie de ce papier, il faut comprendre la différence entre les degrés des équations :

• Degré 1 (Linéaire) : C'est une ligne droite. Trop simple pour cacher des secrets complexes.
• Degré 2 (Quadratique) : C'est une courbe (comme une parabole). On peut encore la maîtriser. C'est comme un labyrinthe avec un plan.
• Degré 3 (Cubique) : C'est une surface tordue, complexe. C'est ici que la magie opère.

L'analogie du "Sélecteur" :
Imaginez que vous construisez un mur de briques (les équations).

• La plupart des briques sont carrées (degré 2).
• Mais pour activer une partie du mur, vous avez besoin d'un interrupteur (un "sélecteur").
• Quand vous appuyez sur l'interrupteur (degré 1) pour activer une brique complexe (degré 2), le résultat est une interaction de degré 3.

C'est exactement ce que fait l'auteur : il utilise des interrupteurs simples pour activer des vérifications complexes. Le résultat final est une seule équation géante de degré 3.

3. La Méthode : Le "Pliage" sans Casser

Le défi technique était énorme : comment prendre des milliers de petites équations (pour vérifier chaque ligne d'une preuve) et les transformer en UNE SEULE équation sans que celle-ci ne devienne trop complexe (degré 4, 5, etc.) ?

L'auteur utilise une astuce ingénieuse basée sur les nombres de Fibonacci (une suite de nombres où chaque nombre est la somme des deux précédents : 1, 1, 2, 3, 5, 8...).

• L'analogie du "Code-barres" : Imaginez que chaque petite équation est un chiffre dans un code-barres.
• L'auteur utilise les nombres de Fibonacci comme des "poids" pour empiler ces chiffres les uns sur les autres sans qu'ils ne se mélangent (sans "retenue" ou carry).
• Cela permet de coller toutes les équations ensemble en une seule, tout en gardant la complexité maximale à 3. C'est comme plier une feuille de papier infiniment complexe pour qu'elle rentre dans une boîte de taille fixe, sans la déchirer.

4. Le Résultat : L'Impossibilité de la Machine Parfaite

Une fois cette équation géante (le "Polynôme Universel Cubique") construite, l'auteur applique un raisonnement célèbre (le diagonal de Gödel) :

1. Imaginons qu'il existe un ordinateur capable de résoudre n'importe quelle équation cubique.
2. On prend ce programme et on l'applique à lui-même (en le transformant en équation).
3. On crée une équation qui dit : "Je n'ai pas de solution si et seulement si l'ordinateur dit que j'en ai une."
4. Résultat : L'ordinateur est coincé. Il ne peut pas répondre sans se contredire.

Conclusion simple : Il est mathématiquement impossible de créer un programme qui résout toutes les équations cubiques. C'est une barrière fondamentale de l'univers mathématique.

5. Pourquoi c'est important ?

Avant ce papier, on savait que les équations de degré 4 étaient indécidables, et que les équations de degré 2 étaient décidables. Mais le degré 3 restait une zone d'ombre. Est-ce qu'il est décidable ou non ?

Ce papier ferme la porte : Le degré 3 est indécidable.

L'auteur a même écrit un programme informatique (en OCaml et Rocq) qui a généré concrètement cette équation géante avec des millions de variables, prouvant que ce n'est pas juste une théorie abstraite, mais quelque chose de réel et de calculable.

En Résumé

Ce papier est comme la découverte d'une frontière infranchissable.

• Avant la frontière (Degré 1 et 2) : On peut tout calculer.
• Après la frontière (Degré 3 et plus) : Le chaos règne, et aucune machine ne peut prédire l'avenir.
• La contribution : L'auteur a construit le pont exact qui mène à cette frontière, prouvant que dès qu'on touche le "cubique", on bascule dans l'indécidable.

C'est une victoire de la logique : en construisant soigneusement une équation de degré 3, on a prouvé qu'il existe des vérités mathématiques que l'on ne pourra jamais vérifier automatiquement.

Résumé technique

1. Problème et Contexte

L'article s'attaque à un problème fondamental de la théorie des nombres et de la logique mathématique : déterminer la complexité de la satisfaisabilité des équations diophantiennes (solutions entières non négatives).

• Contexte historique : Le théorème de MRDP (Matiyasevich-Robinson-Davis-Putnam) a établi que la satisfaisabilité diophantienne générale est indécidable ($\Sigma^0_1$-complète). Cependant, les constructions classiques (comme celles de Jones) produisent des équations de degré 4 ou plus, avec un grand nombre de variables.
• Le problème ouvert : Il était connu que le cas quadratique (degré 2) était décidable pour certaines formes structurées, et que le cas général de degré 4 était indécidable. La question de savoir si le degré 3 (cubique) suffisait pour l'indécidabilité, et si une seule équation universelle de degré 3 pouvait exister dans un nombre fixe de variables, restait ouverte.
• Objectif de l'article : Prouver que la satisfaisabilité d'une unique équation diophantienne de degré total $\le 3$ sur $\mathbb{N}$, où le nombre de variables est encodé dans l'instance, est $\Sigma^0_1$-complète (et donc indécidable).

2. Méthodologie

L'auteur propose une approche constructive et mécanisée, évitant les réductions « boîte noire » complexes. La méthodologie repose sur trois couches conceptuelles :

A. Arithmétique des Registres (RA) et Codage

• Cadre logique : L'article utilise l'arithmétique bornée $I\Delta_0 + B\Sigma_1$ restreinte au langage sans multiplication ($L_{RA} = \{0, S, +, =\}$). La multiplication est représentée comme une relation $\Sigma_1$ via l'addition itérée.
• Codage des traces : Pour éviter les problèmes de retenue (carries) qui complexifient les contraintes diophantiennes, l'auteur utilise une fonction d'appariement sans retenue basée sur la représentation de Zeckendorf (système de nombres de Fibonacci). Cela permet de coder des séquences finies (traces de preuves) de manière injective et primitive récursive, en séparant les bandes de fréquences des composantes.

B. Compilation Primitive Récursive

• Compilateur uniforme : Un compilateur primitif récursive $\varphi \mapsto S_\varphi$ transforme le code d'une sentence arithmétique (ou d'une preuve) en un système fini d'équations diophantiennes.
• Contrôle local du degré :
  • Les vérifications syntaxiques et les règles d'inférence (axiomes, modus ponens) sont compilées en contraintes quadratiques (degré $\le 2$).
  • Le degré 3 n'apparaît que lors de l'activation d'une obligation quadratique par un sélecteur linéaire (variable binaire). C'est le seul mécanisme introduisant le terme cubique.
• Agrégation : Le système fini d'équations est réduit à une unique équation via une technique d'agrégation « mixte » (mixed-radix) utilisant des bandes de Fibonacci. Contrairement à la somme de carrés (qui doublerait le degré), cette méthode préserve le degré 3 en utilisant l'unicité de la représentation des chiffres dans une base suffisamment grande.

C. Mécanisation et Preuve Formelle

• Outil : Le développement est entièrement mécanisé dans Rocq (un assistant de preuve, probablement une variante de Coq ou un fork).
• Vérification : Le compilateur, les bornes de degré et la correspondance sémantique entre la vérification de preuves et la satisfaisabilité de l'équation sont vérifiés par le noyau.
• Extraction : Le code est extrait en OCaml pour générer des artefacts concrets (tables de coefficients).

3. Contributions Clés

1. Théorème de Complétude $\Sigma^0_1$ pour le Degré 3 :
   L'article prouve formellement que le problème de décision $HN(3, n)$ (satisfaisabilité d'une équation de degré 3 avec $n$ variables) est indécidable. Plus précisément, il existe une équation universelle de degré 3.

2. Construction d'une Équation Universelle Explicite :
   L'auteur fournit une équation universelle concrète avec 9 692 variables (selon la définition 6.1.1). Les coefficients de cette équation sont publiés sous forme de table de coefficients vérifiables.

3. Réduction Directe sans MRDP :
   Contrairement aux approches antérieures qui composaient MRDP avec des techniques de « blindage » (Shielding) de Jones, cette construction encode directement la vérification de preuves dans des contraintes polynomiales, offrant un contrôle précis du degré à chaque étape.

4. Preuve Mécanisée et Certificats :
   La preuve n'est pas seulement théorique ; elle est assistée par ordinateur. Le Rocq vérifie que le compilateur émet bien des équations de degré $\le 3$ et que la réduction préserve la satisfaisabilité. Des tables de coefficients « épinglées » (pinned) avec des sommes de contrôle (digests) garantissent l'intégrité des artefacts générés.

4. Résultats Principaux

• Indécidabilité : La satisfaisabilité d'une seule équation diophantienne de degré 3 sur $\mathbb{N}$ est indécidable.
• Universalité Bornée : Pour toute borne de ressources $k$ (longueur de preuve, largeur de chiffre), il existe une équation cubique $U_k$ telle que la satisfaisabilité bornée de $U_k$ est équivalente à l'existence d'une preuve de taille $k$.
• Transition Décidable/Indécidable : Chaque « tranche » bornée (avec un nombre fixe de variables et une borne de recherche) est décidable par énumération finie. L'indécidabilité émerge de l'union non calculable de ces tranches, ce qui empêche l'existence d'une fonction de bornage calculable unique.
• Nombre de Variables : L'article établit une borne supérieure de 1769 variables pour une équation universelle de degré 3 (via une réduction depuis le cas quartique de Jones), mais fournit une construction effective avec 9 692 variables pour un artefact spécifique.

5. Signification et Implications

• Résolution d'un Problème Ouvert : L'article résout la question ouverte posée par Jones (1980) concernant le degré 3, comblant le fossé entre le cas quadratique décidable et le cas quartique indécidable.
• Nouvelle Compréhension de la Complexité : L'article suggère que le seuil de degré 3 n'est pas un accident combinatoire, mais correspond au point où les ressources logiques nécessaires pour définir l'indécidabilité (via l'auto-référence et les gadgets de garde) coïncident avec celles nécessaires pour la provoquer.
• Méthodologie de Preuve : L'approche par mécanisation complète (compilateur vérifié + extraction d'artefacts) offre un nouveau standard de rigueur pour les problèmes de complexité diophantienne, passant de l'existence théorique à la construction effective et vérifiable.
• Conjecture du « Gap Diophantien » : L'auteur émet l'hypothèse que toute théorie formelle suffisamment forte incapable de prouver la décidabilité ou l'indécidabilité du degré 3 pour un petit nombre de variables (ex: $HN(3, 2)$) illustre une forme d'imprédicativité fondamentale : la frontière de l'indécidabilité ne peut être spécifiée de l'intérieur sans la traverser.

En résumé, ce travail démontre que la complexité computationnelle maximale (indécidabilité) peut être encapsulée dans une structure mathématique aussi simple qu'une unique équation cubique, et fournit les outils formels et les données concrètes pour le vérifier.