🔢 mathematics

Lean-verified lower bounds for the Shannon capacity of odd cycles

Cet article présente de nouvelles bornes inférieures, entièrement formalisées en Lean, pour les capacités de Shannon de plusieurs petits cycles impairs ( $C_7, C_{11}, C_{13}, C_{15}, C_{19}, C_{21}, C_{23}$ ) dérivées d'une procédure itérative basée sur les méthodes récentes de Gao et Itty et al.

Auteurs originaux : Pjotr Buys, Sven Polak, Jeroen Zuiddam

Publié 2026-08-03

📖 8 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Pjotr Buys, Sven Polak, Jeroen Zuiddam

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 d'envoyer un message secret à travers une ville bruyante et chaotique. La ville est pleine de distractions, et parfois votre signal se mélange avec les mauvais noms de rues. Dans le monde de la théorie de l'information, c'est un problème bien réel : comment envoyer des données parfaitement sans aucune erreur ? Dans les années 1950, un mathématicien nommé Claude Shannon a découvert que si vous avez un canal « bruyant », vous pouvez tout de même envoyer des messages parfaitement, mais seulement si vous êtes habile dans la manière de regrouper vos lettres. Il a introduit un concept appelé « capacité de Shannon », qui est essentiellement un score indiquant la vitesse maximale à laquelle vous pouvez envoyer des messages parfaits à travers un type spécifique de réseau bruyant.

Pour visualiser cela, imaginez un jeu joué sur la carte d'une ville. La carte est un graphe, où les intersections sont des points et les rues sont des lignes. Certaines rues sont « sûres » pour voyager ensemble, tandis que d'autres sont dangereuses et provoqueront un accident si vous les mélangez. Le but est de choisir le plus grand groupe possible d'intersections (un « ensemble indépendant ») que vous pouvez visiter sans jamais emprunter une rue dangereuse entre deux d'entre elles. La « capacité de Shannon » pose une question délicate : si vous jouez ce jeu non pas une seule fois, mais en empilant plusieurs copies de la carte les unes sur les autres pour créer une ville géante et multidimensionnelle, de combien votre groupe sûr peut-il s'agrandir ? Pour certaines formes, nous connaissons la réponse. Pour d'autres, spécifiquement les boucles de forme impaire (comme un pentagone ou un heptagone), la réponse est un mystère depuis des décennies. C'est comme connaître la limitation de vitesse sur une route droite, mais n'avoir aucune idée de la vitesse à laquelle on peut rouler sur une piste sinueuse à sept angles.

Cet article traite de l'élucidation de ce mystère pour plusieurs de ces pistes sinueuses et complexes (à sept angles et plus). Les auteurs, une équipe de mathématiciens et d'informaticiens, ont trouvé de nouvelles façons, légèrement plus rapides, d'envoyer des messages parfaits à travers ces boucles spécifiques. Ils n'ont pas simplement deviné ; ils ont utilisé une recette astucieuse, étape par étape, pour construire des groupes de plus en plus grands d'intersections sûres. Pour s'assurer de ne commettre pas une seule erreur dans leur calcul complexe, ils ont utilisé un arbitre numérique super strict nommé « Lean » pour vérifier chaque étape de leur travail. Le résultat ? Ils ont prouvé que pour ces boucles impaires spécifiques, la vitesse maximale de communication parfaite est plus élevée que ce qui avait été calculé précédemment.

Le jeu des intersections sûres

Analysons ce que les auteurs ont réellement fait. Ils étudiaient des graphes qui ressemblent à de simples anneaux avec un nombre impair de points : un anneau de 7, un anneau de 11, un anneau de 13, et ainsi de suite. Pendant longtemps, les mathématiciens ont connu la « limite de vitesse » (la capacité de Shannon) pour un anneau de 5 points. Mais pour les anneaux de 7 points ou plus, la réponse est restée plongée dans le brouillard. Nous savions qu'elle était au moins égale à un certain nombre, mais nous ne savions pas si elle pouvait être plus élevée.

Les auteurs ont utilisé une méthode qui ressemble à une recette magique pour faire croître votre groupe sûr. Imaginez que vous avez un petit club d'amis sûrs (un ensemble de points) sur une seule carte. L'article décrit un « théorème de produit », qui est comme une machine qui prend deux de ces cartes et les fracasse ensemble pour créer une nouvelle carte plus grande. Si vous avez un club sûr sur la première carte et un club sûr sur la seconde, vous pouvez les combiner pour créer un club sûr sur la nouvelle, plus grande carte. Généralement, la taille de ce nouveau club est simplement la taille du premier club multipliée par la taille du second. Mais les auteurs ont trouvé un « gadget » ou une astuce particulière. En utilisant un motif de connexions spécifique (appelé « tuple valide »), ils ont pu rendre le nouveau club plus grand que ce que la simple multiplication suggérerait.

Voyez cela ainsi : si vous avez une équipe de 2 personnes qui peuvent travailler ensemble sans se disputer, et que vous combinez deux telles équipes, vous pourriez vous attendre à une équipe de 4 personnes. Mais avec cette astuce spéciale, les auteurs ont trouvé un moyen de combiner ces équipes pour obtenir une équipe de 5 personnes qui s'entendent parfaitement. En répétant cette astuce encore et encore, en empilant les cartes de plus en plus haut, ils ont pu faire croître ces équipes sûres en groupes massifs.

Les nouveaux records

L'équipe a appliqué cette recette à sept anneaux impairs différents : ceux de 7, 11, 13, 15, 19, 21 et 23 points. Pour chacun d'eux, ils sont partis d'un groupe sûr connu et ont fait tourner leur machine d'empilement de nombreuses fois. Le résultat était une nouvelle borne inférieure pour la capacité de Shannon.

Voici ce qu'ils ont trouvé, avec les chiffres exactement tels qu'ils les ont calculés :

Pour l'anneau de 7 points, ils ont prouvé que la capacité est d'au moins 3,258805369885. C'est un tout petit peu plus élevé que la meilleure estimation précédente.
Pour l'anneau de 11 points, le nouveau plancher est de 5,294502522149.
Pour l'anneau de 13 points, ils ont repoussé la limite à 6,302455083464.
Pour l'anneau de 15 points, le nombre est de 7,301600534487.
Pour l'anneau de 19 points, ils ont atteint 9,357192705918.
Pour l'anneau de 21 points, la borne est de 10,342455853338.
Et pour l'anneau de 23 points, ils ont trouvé une capacité d'au moins 11,328224257774.

Ces chiffres peuvent ressembler à une suite de chiffres aléatoires, mais dans le monde de la théorie de l'information, ils représentent une amélioration concrète. Cela signifie que pour ces réseaux spécifiques, nous savons désormais avec certitude que nous pouvons envoyer des messages un peu plus vite que ce que nous pensions possible auparavant.

L'arbitre numérique

Ce qui rend cet article spécial, ce n'est pas seulement les chiffres, mais la manière dont ils ont été obtenus. Les mathématiques impliquées sont incroyablement complexes, impliquant d'énormes ensembles de données et des milliers d'étapes. C'est le genre de travail où un humain pourrait facilement manquer une infime erreur. Pour résoudre cela, les auteurs ont écrit l'intégralité de leur preuve dans un langage informatique appelé Lean.

Considérez Lean comme un arbitre numérique hyper strict qui n'accepte pas le « je pense que c'est juste » ou « ça semble correct ». Il exige une preuve logique absolue pour chaque étape. Si les auteurs avaient commis une erreur dans leur logique, Lean s'arrêterait et dirait : « Non, cela n'en découle pas ». Le fait que l'article soit « vérifié par Lean » signifie qu'un ordinateur a vérifié chaque ligne de leur raisonnement et a confirmé que leurs nouvelles bornes sont mathématiquement solides. Ils n'ont pas seulement simulé les résultats ; ils ont formellement prouvé les résultats.

Les auteurs mentionnent également qu'ils ont utilisé des modèles de langage étendus (comme les chatbots d'IA avancés) pour les aider à trouver les motifs et les recettes initiaux pour ces groupes sûrs. C'est un peu comme avoir un assistant créatif qui suggère une idée farfelue, puis les mathématiciens utilisent leurs outils rigoureux pour tester si cette idée tient la route. Dans ce cas, l'IA a suggéré un chemin, et l'équipe humain-mathématicien-IA l'a parcouru jusqu'à une ligne d'arrivée vérifiée.

Pourquoi cela importe

Vous pourriez vous demander : « Et alors ? On sait juste que le chiffre est un peu plus élevé. » La réponse réside dans la nature du problème. Pendant des décennies, la capacité de ces anneaux impairs a été une question ouverte. Nous savions que la réponse se trouvait quelque part entre une limite inférieure et une limite supérieure (la borne de Lovász), mais nous ne pouvions pas la fixer précisément. Chaque fois que nous poussons la limite inférieure vers le haut, même d'une infime fraction, nous réduisons l'écart. Nous nous rapprochons de la véritable réponse.

Ce travail montre que même pour des problèmes bloqués depuis longtemps, il reste de la place pour l'amélioration si vous avez les bons outils et la patience de vérifier votre travail avec les normes les plus rigoureuses possibles. Les auteurs n'ont pas résolu tout le mystère de la capacité de Shannon pour tous les anneaux impairs, mais ils ont dissipé le brouillard de certains coins spécifiques, prouvant que pour les anneaux de 7, 11, 13, 15, 19, 21 et 23, nous pouvons communiquer un peu plus vite que ce que nous croyions auparavant.

Résumé technique : Bornes inférieures vérifiées par Lean pour la capacité de Shannon des cycles impairs

Énoncé du problème
L'article traite du problème ouvert de longue date consistant à déterminer la capacité de Shannon, $\Theta(G)$ , pour les cycles impairs $C_n$ où $n \geq 7$ . La capacité de Shannon est définie par $\Theta(G) := \sup_{d \geq 1} \alpha(G^{\boxtimes d})^{1/d}$ , où $\alpha$ désigne le nombre d'indépendance et $\boxtimes$ le produit fort de graphes. Alors que Lovász a déterminé $\Theta(C_5) = \sqrt{5}$ en utilisant la fonction thêta $\vartheta(G)$ , les capacités exactes pour tous les cycles impairs de longueur sept ou plus demeurent inconnues. Le défi principal réside dans la recherche d'ensembles indépendants plus grands dans les puissances fortes supérieures de ces cycles afin d'améliorer les bornes inférieures connues.

Méthodologie
Les auteurs emploient une procédure itérative basée sur une « construction de gadget » et un « lemme de produit » récemment proposé par Gao (2026), lequel s'appuie lui-même sur les méthodes d'Itty, Rosin, Carstensen et Reichman (2026). Le cœur de la méthodologie implique :

Tuples valides : Pour un graphe $G$ , un tuple valide $\tau = (I, S, f_0, f_1, X)$ est défini, où $I$ est un ensemble indépendant, $S \subseteq I$ , et $f_0, f_1$ sont des applications spécifiques satisfaisant des contraintes de voisinage strictes. Ce tuple génère un « profil » $\Pi(\tau) = (|I|, |S|, |X|, |X \setminus (N_G[f_0(S)] \cup N_G[f_1(S)])|)$ .
Opération de produit : Une opération binaire $\star$ est définie sur les profils. Le Théorème 1 établit que si $\tau$ et $\tau'$ sont des tuples valides pour les graphes $G$ et $H$ , il existe un tuple valide pour le produit fort $G \boxtimes H$ dont le profil est le produit $\star$ des profils individuels.
Construction itérative : En partant d'un tuple valide découvert par calcul dans une puissance spécifique d'un cycle impair, les auteurs appliquent de manière itérative le produit $\star$ pour générer des profils pour des puissances supérieures. Ce processus construit des ensembles indépendants dans les puissances fortes $C_n^{\boxtimes d}$ qui sont plus grands que ceux obtenables par de simples produits cartésiens des ensembles indépendants de base.
Vérification formelle : Une composante critique de la méthodologie est la formalisation complète de ces bornes dans l'assistant de preuve Lean. Les tuples de base (ensembles $I, S, X$ et applications $f_0, f_1$ ) sont encodés comme des littéraux explicites, et leur validité est vérifiée mécaniquement dans l'environnement Lean.

Contributions clés et résultats
L'article présente de nouvelles bornes inférieures améliorées pour les sept petits cycles impairs ( $C_7, C_{11}, C_{13}, C_{15}, C_{19}, C_{21}, C_{23}$ ). Ces bornes sont dérivées de l'identification de tuples valides de base spécifiques et de l'application de la procédure de produit itératif. Les résultats sont :

$\Theta(C_7)$ : Amélioré à $\geq 3,258805369885\dots$ (précédemment $3,2587891\dots$ par Gao 2026). La construction utilise un tuple de base dans $C_7^{\boxtimes 5}$ itéré jusqu'à la puissance 200.
$\Theta(C_{11})$ : Amélioré à $\geq 5,294502522149\dots$ (précédemment $5,2897736\dots$ par Itty et al. 2026). Le tuple de base est dans $C_{11}^{\boxtimes 3}$ , itéré jusqu'à la puissance 174.
$\Theta(C_{13})$ : Amélioré à $\geq 6,302455083464\dots$ (précédemment $6,3001091\dots$ par Itty et al. 2026). Le tuple de base est dans $C_{13}^{\boxtimes 6}$ , itéré jusqu'à la puissance 432.
$\Theta(C_{15})$ : Amélioré à $\geq 7,301600534487\dots$ (précédemment $7,3013990\dots$ par Itty et al. 2026). Le tuple de base est dans $C_{15}^{\boxtimes 4}$ , itéré jusqu'à la puissance 4096.
$\Theta(C_{19})$ : Amélioré à $\geq 9,357192705918\dots$ (précédemment $9,3571200\dots$ par Baumert et al. 1971). Le tuple de base est dans $C_{19}^{\boxtimes 4}$ , itéré jusqu'à la puissance 16384.
$\Theta(C_{21})$ : Amélioré à $\geq 10,342455853338\dots$ (précédemment $10,3422729\dots$ par Baumert et al. 1971). Le tuple de base est dans $C_{21}^{\boxtimes 4}$ , itéré jusqu'à la puissance 4096.
$\Theta(C_{23})$ : Amélioré à $\geq 11,328224257774\dots$ (précédemment $11,3278379\dots$ par Baumert et al. 1971). Le tuple de base est dans $C_{23}^{\boxtimes 4}$ , itéré jusqu'à la puissance 2048.

Les améliorations, bien que numériquement faibles (allant de $10^{-5}$ à $10^{-3}$ ), représentent l'état de l'art actuel pour ces cycles spécifiques.

Signification et revendications
L'article revendique sa signification principalement par la rigueur de la vérification de ces résultats. En formalisant l'intégralité de la construction et des bornes résultantes dans Lean, les auteurs garantissent que les arguments combinatoires complexes et les constructions d'ensembles spécifiques sont exempts d'erreur humaine. Ce travail suit la trajectoire des recherches récentes utilisant des modèles de langage étendus (LLM) pour découvrir les constructions initiales (comme vu dans [IRCR26] et [Gao26]), mais se distingue en fournissant une preuve entièrement formalisée et vérifiée par machine de la validité des tuples de base et de la justesse de l'application du lemme de produit itératif. Les auteurs ne prétendent pas avoir résolu le problème général de la capacité de Shannon pour les cycles impairs, ni proposer de nouveaux cadres théoriques au-delà de l'application du lemme de produit existant de Gao ; ils fournissent plutôt les meilleures bornes inférieures numériques actuellement connues pour ces instances spécifiques, vérifiées avec une certitude mathématique.

Le jeu des intersections sûres

Les nouveaux records

L'arbitre numérique

Pourquoi cela importe

Articles similaires