🔢 mathematics

Formal Foundations and Proof-Carrying Certificates for q-ary Covering Codes in Lean 4

Cet article présente une formalisation de la théorie élémentaire des codes de couverture q-aires dans Lean 4, établissant une fondation réutilisable et auditable avec des certificats porteurs de preuves pour vérifier les bornes supérieures et inférieures sur les nombres de couverture.

Auteurs originaux : Andreas Florath

Publié 2026-06-09

📖 6 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 essayez de couvrir un échiquier géant et multidimensionnel avec un nombre limité de « filets de sécurité ».

Dans le monde des mathématiques, c'est le problème des codes de couverture. Vous avez une grille de positions possibles (comme un échiquier, mais cela pourrait être en 3D, 4D ou même de dimensions supérieures). Vous voulez placer un petit nombre de « centres » sur votre grille. La règle est que chaque case de l'échiquier doit se trouver à une certaine distance (disons, un pas) d'au moins un de vos centres.

La grande question est : quel est le nombre absolument minimum de centres dont vous avez besoin pour couvrir l'échiquier entier ?

Ce document, écrit par Andreas Florath, ne cherche pas à établir un nouveau record du plus petit nombre de centres. Au lieu de cela, il construit un coffre-fort numérique inviolable pour prouver que les nombres que nous connaissons déjà sont corrects.

Voici une décomposition des idées de ce document en utilisant des analogies simples :

1. Le « Certificat porteur de preuve » (Le Ticket d'Or)

Habituellement, lorsqu'un mathématicien dit : « J'ai trouvé un code avec 73 centres qui couvre l'échiquier », il vous montre une liste de nombres. Vous devez alors le croire, ou passer des heures à vérifier les calculs vous-même.

Ce document introduit un « Certificat porteur de preuve ». Ne voyez pas cela comme une simple liste de nombres, mais comme un Ticket d'Or doté d'un tour de magie auto-vérifiable intégré.

Le Ticket : Il dit : « Voici un ensemble de 73 centres. »
Le Tour de Magie : Le ticket contient un petit robot automatisé (écrit dans un langage appelé Lean 4) qui vérifie instantanément chaque case de l'échiquier pour confirmer : « Oui, cette case est couverte. Oui, cette case est couverte. Oui, toutes sont couvertes. »
Le Résultat : Vous n'avez pas à faire confiance à l'auteur. Vous lancez simplement le robot. Si le robot affiche « Succès », la preuve est 100 % garantie mathématiquement.

2. Le « Puzzle en deux parties »

Pour prouver que vous avez le nombre exact (parfait) de centres, vous devez résoudre deux puzzles différents simultanément :

La Borne Supérieure (La Construction) : « Je peux couvrir l'échiquier avec 73 centres. » (Vous montrez la liste).
La Borne Inférieure (La Tâche Impossible) : « Il est impossible de couvrir l'échiquier avec 72 centres. » (Vous prouvez que peu importe comment vous essayez, il restera toujours un trou).

Le document construit un système où ces deux puzzles sont des pièces séparées. Vous pouvez avoir un certificat pour les « 73 » et un certificat distinct pour « l'impossibilité avec 72 ». Lorsqu'ils se rencontrent, ils s'emboîtent pour former une réponse exacte et parfaite.

3. Les « Legos » des Mathématiques

L'auteur a construit une immense bibliothèque de briques de Lego (des règles formelles).

Certaines briques sont simples : « Si vous couvrez un petit échiquier, vous pouvez en couvrir un plus grand en ajoutant quelques pièces supplémentaires. »
D'autres sont complexes : « Si vous combinez deux types d'échiquiers différents, voici exactement comment les règles de couverture changent. »

La beauté de ce document est que ces briques sont interchangeables. Si quelqu'un d'autre trouve une nouvelle façon de couvrir un échiquier, il peut simplement emboîter sa nouvelle brique dans cette structure de Lego existante, et l'ensemble du système la vérifiera automatiquement.

4. La « Base de données de la Vérité »

Le document inclut une Base de données porteuse de preuve. Imaginez un livre de bibliothèque où, au lieu d'imprimer simplement la réponse « La réponse est 7 », le livre inclut l'enregistrement vidéo de la preuve.

Si vous cherchez un nombre dans cette base de données, il ne vous donne pas seulement un chiffre. Il vous donne la trace (la vidéo étape par étape) de la manière dont ce nombre a été prouvé.
Vous pouvez rejouer cette vidéo dans le système Lean 4, et il relancera la preuve depuis le début pour s'assurer qu'elle tient toujours la route.

5. L'exemple du « Football Pool »

Le document utilise une analogie du monde réel pour expliquer le problème : le Football Pool.
Imaginez que vous pariez sur 8 matchs de football. Chaque match a 3 résultats possibles (Victoire, Nul, Défaite). Vous voulez acheter un ensemble de tickets de pari.

L'Objectif : Peu importe les résultats réels, vous voulez garantir qu'au moins un de vos tickets est « proche » (par exemple, avec seulement une erreur de prédiction).
Les Mathématiques : Combien de tickets devez-vous acheter pour garantir cela ?
Le Rôle du Document : Le document prend une solution célèbre et publiée pour ce problème (où quelqu'un a trouvé un ensemble de 486 tickets) et la transforme en un certificat vérifiable par machine. Il prouve, sans l'ombre d'un doute, que 486 tickets fonctionnent.

Ce que ce document affirme réellement (et ce qu'il ne fait pas)

Il AFFIRME : Qu'il a construit une fondation solide et réutilisable (une « fondation formelle ») où les preuves de codes de couverture peuvent être stockées, vérifiées et combinées automatiquement. Il a vérifié plusieurs nombres spécifiques connus (comme les 486 tickets pour le problème des 8 matchs) en utilisant ce nouveau système.
Il NE CLAIME PAS : Qu'il a trouvé un nouveau record du plus petit nombre de tickets nécessaires. Il ne prétend pas non plus résoudre le problème pour tous les scénarios possibles. C'est un document de construction d'outils, et non un document de battre des records.

La Vue d'Ensemble

Considérez ce document comme la construction d'un coffre-fort à haute sécurité pour les vérités mathématiques. Auparavant, si vous vouliez vérifier un code de couverture complexe, vous deviez faire confiance à un humain ou à un programme informatique qui pourrait contenir un bug. Désormais, grâce à ce document, vous disposez d'un système où la preuve elle-même est un logiciel que vous pouvez exécuter pour vérifier la vérité instantanément. Cela transforme le « Je pense que c'est juste » en « L'ordinateur a prouvé que c'est juste ».

Résumé Technique : Fondations Formelles et Certificats de Preuve pour les Codes de Couverture $q$ -aires dans Lean 4

Énoncé du Problème
Les codes de couverture dans les espaces de Hamming finis cherchent l'ensemble le plus petit de mots (mots de code) tel que l'union de leurs boules de Hamming de rayon $r$ couvre l'espace entier $A^n$ . La quantité centrale est le nombre de couverture $q$ -aire $K_q(n,r)$ , défini comme la taille minimale d'un tel code. Bien que la définition soit élémentaire, la détermination des valeurs exactes ou de bornes serrées pour $K_q(n,r)$ repose généralement sur un mélange de constructions explicites, d'arguments de dénombrement, de relations récursives et de recherches informatiques. Un défi important dans ce domaine est que les énoncés exacts $K_q(n,r) = k$ nécessitent deux composantes indépendantes : une construction explicite prouvant une borne supérieure ( $K_q(n,r) \le k$ ) et une preuve qu'aucun code plus petit n'existe (une borne inférieure $K_q(n,r) \ge k$ ). Ces composantes provenant souvent de sources disparates, la vérification des valeurs exactes peut s'avérer difficile à auditer.

Méthodologie
L'article présente une formalisation de la théorie élémentaire des codes de couverture dans le prouveur de théorèmes Lean 4. La méthodologie est caractérisée par trois choix de conception fondamentaux :

Représentation des Mots : Les mots sont modélisés comme des fonctions dépendantes d'un type de coordonnée vers un type d'alphabet. L'espace de Hamming $q$ -aire général de longueur $n$ est représenté comme Fin n → Fin q. Cette représentation fonctionnelle préserve une interface générale pour les types de coordonnées abstraits tout en simplifiant la spécialisation $q$ -aire.
Prédicats de Type Certificat : Au lieu de définir $K_q(n,r)$ $K_{q} (n, r)$ comme une fonction de minimisation non calculable, la formalisation utilise des prédicats logiques pour représenter des assertions sur les nombres de couverture.
- KUpper r k : Asserte l'existence d'un code de couverture fini de taille au plus $k$ (borne supérieure).
- KLower r k : Asserte que tout code de couverture fini a une taille d'au moins $k$ (borne inférieure).
- KSpec r k : Combine les deux pour affirmer l'exactitude ( $K_q(n,r) = k$ ).
  Cette approche modulaire permet d'assembler indépendamment des bornes supérieures et inférieures provenant de sources différentes.
Base de Données Portant Preuve : L'article implémente une base de données où les bornes stockées ne sont pas de simples valeurs numériques mais des objets « portant preuve ». Chaque entrée inclut une trace de dérivation. Rejouer cette trace dans Lean reconstruit une preuve formelle du prédicat QaryKUpper ou QaryKLower correspondant. Le système distingue les théorèmes mathématiques écrits à la main (vérifiés par le noyau) et les données générées (producteurs non fiables dont la sortie est validée via le rejeu de trace).

Contributions Clés
L'article établit une fondation réutilisable et auditable pour les certificats de codes de couverture vérifiés par machine. Ses contributions spécifiques incluent :

Infrastructure Formelle : Un cadre complet dans Lean 4 pour les espaces de Hamming finis, la distance de Hamming, les boules fermées et les prédicats de couverture, gérant rigoureusement les cas limites (ex: $q=0$ , $n=0$ , $r \ge n$ ) au sein des définitions plutôt que comme des conventions informelles.
Résultats Analytiques : Preuves formelles de la formule du volume de la boule de Hamming $q$ -aire et de la borne inférieure classique de couverture de sphère. La borne de couverture de sphère est encapsulée dans une fonction calculable sphereLower qui génère des certificats de borne inférieure certifiés.
Théorèmes Structurels : Formalisation de cas exacts élémentaires (ex: $K_q(n,0) = q^n$ , $K_q(n, n-1) = q$ ) et de constructions structurelles, incluant un théorème de couverture de produit et diverses relations de voisinage (ponctionnement, allongement, projection d'alphabet et concaténation) qui transportent les bornes entre les triplets de paramètres.
Étude de Cas (Van Laarhoven et al.) : Un flux de travail de bout en bout démontrant la formalisation de codes explicites publiés. Les auteurs ont transcrit des codes de couverture d'un article de 1989 (Van Laarhoven et al.) dans Lean, en les encodant sous forme de tableaux compacts pour éviter les limites d'élaboration. Le système a vérifié la propriété de couverture et la cardinalité, produisant des certificats de borne supérieure vérifiés par machine pour $K_3(6,1) \le 73$ , $K_3(7,1) \le 186$ et $K_3(8,1) \le 486$ .
Implémentation de la Base de Données : Une base de données portant preuve contenant 52 822 entrées pour les paramètres $0 \le q \le 21$ , $0 \le n \le 48$ et $0 \le r \le 48$ . Cette base de données inclut des certificats exacts pour de petits cas (ex: $K_2(5,1)=7$ , $K_3(3,1)=5$ ) et des intervalles dérivés du rejeu de trace.

Résultats
La formalisation vérifie avec succès :

La formule du volume de la boule $q$ -aire et la borne inférieure de couverture de sphère.
Des valeurs exactes élémentaires telles que $K_2(5,1)=7$ , $K_2(6,2)=4$ , $K_3(3,1)=5$ et $K_4(3,1)=8$ .
Des bornes supérieures pour le problème ternaire des pools de football dérivées de codes explicites, spécifiquement $K_3(6,1) \le 73$ , $K_3(7,1) \le 186$ et $K_3(8,1) \le 486$ .
Une construction cyclique à deux blocs uniforme prouvant $K_q(3,1) \le \lceil q^2/2 \rceil$ .

Le processus de clôture de la base de données a réussi à propager ces sources primitives à travers des règles de relation certifiées pour générer une table de bornes cohérente. Le système supporte deux modes de preuve : un « mode noyau » utilisant un decide standard pour des garanties de rejeu plus fortes, et un « mode natif » utilisant l'évaluateur compilé de Lean pour un développement plus rapide, avec des frontières de confiance clairement définies pour chacun.

Signification et Revendications
L'article stipule explicitement que sa contribution principale n'est pas la découverte de nouvelles bornes records ou la reproduction de tables de la littérature existante. Au contraire, sa signification réside dans la fourniture d'une interface formelle et d'une fondation auditable pour les certificats de codes de couverture.

Ce travail comble le fossé entre la littérature classique des codes de couverture et les futurs certificats computationnels. En séparant les témoins de bornes supérieures, les arguments de bornes inférieures et les prédicats d'exactitude, la formalisation permet aux résultats issus de constructions explicites, de dénombrements combinatoires et (potentiellement) de solveurs SAT ou de programmation entière de être vérifiés et composés au sein d'un cadre unique de confiance. La nature « portant preuve » de la base de données garantit que chaque borne rapportée peut être tracée jusqu'à une preuve vérifiée par machine, répondant ainsi aux défis de reproductibilité et de vérification inhérents au domaine. L'article se positionne comme une étape fondamentale vers un futur où les résultats de recherche computationnelle pourront être intégrés de manière transparente dans les bibliothèques mathématiques formelles.