🔢 mathematics

A Lean-Certified Proof of $K_8(4, 2) = 23$

Cet article présente une preuve entièrement formalisée dans Lean 4 que la valeur du code de couverture octonaire $K_8(4, 2)$ est égale à 23, établissant la borne supérieure via un code explicite de 23 mots et la borne inférieure en combinant des arguments de comptage de fibres avec des instances de CNF réfutées par LRAT pour démontrer qu'aucune couverture de 22 mots ne peut exister.

Auteurs originaux : Andreas Florath

Publié 2026-06-16

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Andreas Florath

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 essayiez de ranger un ensemble de « filets de sécurité » spéciaux dans une immense pièce à quatre dimensions remplie de millions de points. L'objectif est de s'assurer que chaque point de la pièce se trouve à une courte distance (disons, deux pas) d'au moins un filet de sécurité.

La question que les mathématiciens se posent est la suivante : Quel est le nombre absolument minimum de filets de sécurité dont vous avez besoin pour couvrir toute la pièce ?

Pour un type de pièce spécifique (où chaque dimension possède 8 valeurs possibles), la réponse a été resserrée autour d'une plage minuscule : c'est soit 22 filets, soit 23 filets. Cette publication, écrite par Andreas Florath, prouve de manière définitive que 23 est le chiffre magique. Vous ne pouvez pas le faire avec 22 filets.

Voici comment fonctionne la preuve, décomposée en analogies simples :

1. La preuve en deux parties

Pour prouver que la réponse est exactement 23, l'auteur a dû faire deux choses, comme pour prouver qu'une porte est verrouillée des deux côtés :

La borne supérieure (Montrer que 23 fonctionne) : L'auteur a simplement trouvé une liste spécifique de 23 filets de sécurité et l'a vérifiée par rapport à chaque point de la pièce. C'est comme dire : « Voici une carte de 23 casernes de pompiers ; j'ai parcouru chaque rue et confirmé qu'aucune maison n'est à plus de deux pâtés de maisons d'une caserne. » Cette partie est facile à vérifier car l'auteur a simplement présenté la liste.
La borne inférieure (Montrer que 22 échoue) : C'est la partie difficile. L'auteur a dû prouver qu'il est impossible de couvrir la pièce avec seulement 22 filets. On ne peut pas simplement vérifier toutes les dispositions possibles de 22 filets car il y en a trop (plus que d'atomes dans l'univers). Au lieu de cela, l'auteur a utilisé un tour de logique astucieux pour montrer que toute tentative d'utiliser 22 filets créerait inévitablement un trou.

2. Le travail de détective de la « paire manquante »

Pour prouver que 22 filets ne suffisent pas, l'auteur n'a pas regardé directement les filets. À la place, il a regardé ce qui manquait.

Imaginez que la pièce est une grille géante. Si vous choisissez n'importe quelle paire de coordonnées (comme « sol » et « mur »), vous pouvez examiner toutes les paires de valeurs qui apparaissent dans les filets.

La logique : Si une paire de valeurs spécifique (par exemple, « Sol 3, Mur 5 ») n'apparaît jamais ensemble dans aucun de vos 22 filets, c'est une « paire manquante ».
Le graphe : L'auteur a dessiné une carte (un graphe) pour chaque paire de coordonnées, marquant les combinaisons « manquantes ».
La contradiction : La preuve montre que si vous n'avez que 22 filets, les règles de la géométrie forcent ces cartes de « paires manquantes » à former une forme spécifique et interdite, un « clique » (un nœud serré de connexions manquantes). Mais si cette forme existe, cela signifie qu'il y a un point dans la pièce qui est trop loin de n'importe lequel de vos filets. Par conséquent, 22 filets ne peuvent pas couvrir la pièce.

3. Le puzzle des « blocs »

Lorsque l'auteur a analysé le cas où quelqu'un essaie d'utiliser exactement 22 filets, il a découvert que les filets devraient s'organiser selon une structure très rigide, de type bloc (plus précisément un motif 3 + 3 + 2).

Pensez à essayer de construire un mur avec 22 briques. Les mathématiques montrent que pour éviter les trous, les briques devraient être empilées en trois groupes spécifiques. Cependant, lorsque vous essayez de construire la section finale du mur en utilisant les briques restantes, la géométrie s'effondre. C'est comme essayer de faire entrer une cheville carrée dans un trou rond ; la structure requise pour couvrir la pièce ne peut tout simplement pas exister avec seulement 22 pièces.

4. La vérification informatique « légère »

C'est ici que le papier devient très technologique. Comme la logique de la « paire manquante » implique de vérifier des milliers de petites possibilités (comme un puzzle de Sudoku avec des millions de cellules), l'auteur a utilisé un programme informatique appelé Lean.

Le solveur SAT : L'auteur a utilisé un puissant programme informatique (un solveur SAT) pour vérifier la liste massive de possibilités et dire : « Cette disposition spécifique est impossible. »
Le certificat : Habituellement, nous devons faire confiance à l'ordinateur. Mais ici, l'ordinateur n'a pas seulement dit « Impossible ». Il a produit un certificat (un reçu étape par étape de sa logique).
La vérification : Le programme Lean a ensuite lu ce reçu et a vérifié chaque étape de la logique de l'ordinateur lui-même. Cela signifie que la preuve est vérifiée par machine. Nous n'avons pas à faire confiance au cerveau de l'ordinateur ; nous devons seulement faire confiance à la capacité du programme Lean à lire le reçu, qui est beaucoup plus petit et plus facile à vérifier.

Résumé

Le papier prouve que pour cette pièce spécifique à quatre dimensions avec 8 options par dimension :

23 filets sont suffisants (voici la liste).
22 filets ne sont pas suffisants (voici une preuve logique que toute tentative d'utiliser 22 filets crée un écart inévitable).

Le résultat est une preuve « certifiée par Lean », ce qui signifie que l'argument entier — de la grande logique aux minuscules vérifications informatiques — a été vérifié par un système logiciel mathématique formel, ne laissant aucune place à l'erreur humaine ou au doute. La réponse est exactement 23.

Résumé Technique : Une preuve certifiée par Lean de $K_8(4,2) = 23$

Énoncé du Problème
L'article traite de la détermination du nombre de couverture exact $K_q(n,r)$ , défini comme la taille minimale d'un code de couverture de rayon $r$ dans l'espace de Hamming à $q$ lettres de longueur $n$ . Plus précisément, il résout la valeur pour le cas octonaire de longueur 4 et de rayon 2 : $K_8(4,2)$ . Avant ce travail, les bornes existantes (notamment les tables de Kéri) plaçaient cette valeur dans l'intervalle $[22, 23]$ . La borne inférieure était dérivée de la borne de Rodemich sur le domaine des rois, tandis que la borne supérieure était soutenue par des bornes à grand alphabet. L'objectif était de fermer cet intervalle en prouvant la borne inférieure $K_8(4,2) \ge 23$ .

Méthodologie
La preuve est formalisée dans le prouveur de théorèmes Lean 4 en utilisant la bibliothèque mathlib. Elle emploie une approche de « preuve transportée » où le résultat est établi via deux certificats indépendants : une borne supérieure explicite et une borne inférieure structurelle.

Borne Supérieure ( $K_8(4,2) \le 23$ ) :
Les auteurs fournissent un code explicite composé de 23 mots dans $(\text{Fin } 8)^4$ . La preuve formelle vérifie deux conditions : la cardinalité de l'ensemble est au plus de 23, et chaque mot de l'espace ambiant (4096 mots) est à une distance de Hamming de 2 d'au moins un mot de code. Il s'agit d'une vérification finie exhaustive.
Borne Inférieure ( $K_8(4,2) \ge 23$ ) :
Le cœur de l'article est un argument de non-existence structurelle pour tout code hypothétique $C^*$ avec $|C^*| \le 22$ . La preuve procède par une séquence de réductions :
- Comptage de Fibres : Pour un code hypothétique, les auteurs définissent des « fibres » $C^*_{i,a}$ (mots de code ayant le symbole $a$ à la coordonnée $i$ ). Ils prouvent que chaque fibre doit contenir au moins deux mots. Cela établit une base de 16 mots ( $8 \text{ symboles} \times 2$ ) par coordonnée, laissant un « budget » d'au plus 6 mots excédentaires pour le cas $|C^*|=22$ (ou 5 pour $|C^*| \le 21$ ).
- Graphes de Paires Manquantes : La preuve adopte un point de vue « inverse », analysant quelles paires de symboles sont absentes des projections du code sur les paires de coordonnées. Ces paires manquantes forment des graphes $E_{ij}$ .
- Cas $|C^*| \le 21$ : En utilisant le faible budget excédentaire, les auteurs démontrent, via un comptage combinatoire, que les graphes de paires manquantes doivent contenir un « clique partite quatre simultané » (un ensemble de quatre symboles $a,b,c,d$ tels que les six paires de coordonnées sont manquantes). Le Lemme 7 prouve qu'un tel clique ne peut pas exister dans un code de rayon 2 valide, écartant ainsi les couvertures de taille 21 ou moins.
- Cas $|C^*| = 22$ : Pour le cas restant, la preuve réduit le problème à une classification finie du « profil » des graphes de paires manquantes. Les auteurs montrent que tout profil valide doit présenter une structure spécifique de « bloc commun $3+3+2$ ».
- Intégration SAT/LRAT : La classification de ces profils est trop vaste pour une énumération manuelle. Les auteurs encodent les contraintes (bornes de degré par ligne/colonne et la condition d'absence de clique) en instances de forme normale conjonctive (CNF). Ils utilisent un solveur SAT non fiable pour générer des réfutations de type Linear RAT (LRAT) (preuves d'insatisfaisabilité).
- Vérification Formelle : Lean analyse ces certificats LRAT et rejoue mécaniquement les réfutations pour prouver qu'aucun profil valide n'existe pour une couverture de 22 mots.
- Contradiction Finale : Même si une structure de bloc commun était supposée, les auteurs dérivent une contradiction dans la « composante à 2 symboles » de la structure. Cette composante nécessiterait un tableau binaire de force 2 de longueur 4 avec au plus 4 lignes, ce qui est mathématiquement impossible.

Contributions Clés

Valeur Exacte : L'article établit la valeur exacte $K_8(4,2) = 23$ , fermant l'intervalle précédemment connu $[22, 23]$ .
Borne Inférieure Formalisée : Il fournit une preuve entièrement formalisée dans Lean 4 qui exclut toutes les couvertures de 22 mots. Ceci est réalisé non pas par des arguments de volume, mais par des obstructions structurelles dérivées des comptes de fibres et des graphes de paires manquantes.
Artéfact de Preuve : Le résultat est emballé sous la forme d'un artéfact Lean contenant le code explicite, les lemmes structurels, les instances CNF et les réfutations LRAT. Crucialement, le solveur SAT ne fait pas partie de la base de calcul de confiance ; Lean vérifie les certificats LRAT en interne.
Modèle pour les Bornes Inférieures Computationnelles : L'article introduit un modèle réutilisable pour attacher des preuves produites par des solveurs aux bornes de codes de couverture. Il sépare la « découverte » (solveur non fiable) de la « vérification » (noyau Lean fiable), permettant de résoudre des problèmes de classification finie par voie computationnelle tout en maintenant la correction formelle.

Résultats
Le résultat principal est le théorème $K_8(4,2) = 23$ .

Borne Supérieure : Prouvée par un code explicite de 23 mots.
Borne Inférieure : Prouvée en montrant qu'une couverture de taille 22 mène à une contradiction via un « système de bloc commun $3+3+2$ » forcé, ce qui implique l'existence d'un tableau binaire impossible.
Performance : La vérification formelle mobilise des ressources computationnelles importantes. Le rejeu du fichier de preuve principal en mode noyau a nécessité environ 143 GiB de RAM, tandis que le mode natif a réduit cela à environ 5,5 GiB. La phase de vérification LRAT a pris environ 17 minutes en mode noyau.

Signification et Revendications
L'article revendique sa signification principalement dans le domaine de la mathématique formalisée et de la méthodologie combinant le raisonnement combinatoire avec des certificats computationnels.

Changement Méthodologique : Il démontre que la combinatoire structurelle peut être combinée avec des preuves computationnelles « transportées ». Le solveur SAT est utilisé pour découvrir des obstructions finies, mais le pont mathématique et la vérification de la sortie du solveur sont entièrement gérés par le prouveur de théorèmes.
Frontière de Confiance : Ce travail clarifie la frontière de confiance dans les preuves formelles impliquant des solveurs SAT. Le solveur est non fiable ; le noyau Lean vérifie les certificats LRAT et la déduction logique qui relie ces certificats à l'énoncé du code de couverture.
Scalabilité : Le résultat sert de cas de test pour traiter des problèmes de codes de couverture trop grands pour une preuve manuelle mais suffisamment petits pour être réduits à des problèmes de classification finie solubles par des solveurs SAT.
Absence de Nouvelles Applications : L'article ne revendique pas de nouvelles applications pour la valeur $K_8(4,2)=23$ elle-même, ni ne propose de nouveaux protocoles expérimentaux. Sa contribution est strictement la résolution d'un problème ouvert spécifique dans les tables de théorie des codes et la démonstration d'un flux de travail de vérification formelle pour de tels problèmes.