🔢 mathematics

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

Este artigo apresenta novos limites inferiores, totalmente formalizados em Lean, para as capacidades de Shannon de vários pequenos ciclos ímpares ( $C_7, C_{11}, C_{13}, C_{15}, C_{19}, C_{21}, C_{23}$ ) derivados de um procedimento iterativo baseado em métodos recentes de Gao e Itty et al.

Autores originais: Pjotr Buys, Sven Polak, Jeroen Zuiddam

Publicado 2026-08-03

📖 7 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Pjotr Buys, Sven Polak, Jeroen Zuiddam

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você esteja tentando enviar uma mensagem secreta através de uma cidade barulhenta e caótica. A cidade está cheia de distrações e, às vezes, seu sinal se mistura com nomes de ruas errados. No mundo da teoria da informação, isso é um problema real: como você envia dados perfeitamente sem nenhum erro? Na década de 1950, um matemático chamado Claude Shannon descobriu que, se você tiver um canal "ruidoso", ainda pode enviar mensagens perfeitamente, mas apenas se for inteligente sobre como agrupa suas letras. Ele introduziu um conceito chamado "capacidade de Shannon", que é essencialmente uma pontuação que indica a velocidade máxima na qual você pode enviar mensagens perfeitas através de um tipo específico de rede ruidosa.

Para visualizar isso, imagine um jogo jogado em um mapa da cidade. O mapa é um grafo, onde os cruzamentos são pontos e as ruas são linhas. Algumas ruas são "seguras" para viajar junto, enquanto outras são perigosas e causarão um acidente se você as misturar. O objetivo é escolher o maior grupo possível de cruzamentos (um "conjunto independente") que você possa visitar sem nunca percorrer uma rua perigosa entre quaisquer dois deles. A "capacidade de Shannon" faz uma pergunta difícil: se você jogar este jogo não apenas uma vez, mas empilhando várias cópias do mapa um sobre o outro para criar uma cidade multidimensional gigante, o quanto maior o seu grupo seguro pode ficar? Para algumas formas, sabemos a resposta. Para outras, especificamente os loops de formato ímpar na cidade (como um pentágono ou um heptágono), a resposta tem sido um mistério por décadas. É como conhecer o limite de velocidade em uma estrada reta, mas não ter ideia de quão rápido você pode ir em uma pista sinuosa de sete cantos.

Este artigo trata de desvendar esse mistério para várias dessas pistas complicadas de sete cantos (e maiores). Os autores, uma equipe de matemáticos e cientistas da computação, encontraram novas maneiras, ligeiramente mais rápidas, de enviar mensagens perfeitas através desses loops específicos. Eles não apenas adivinharam; eles usaram uma receita inteligente e passo a passo para construir grupos cada vez maiores de cruzamentos seguros. Para garantir que não cometeram um único erro em sua matemática complexa, eles usaram um árbitro digital super rigoroso chamado "Lean" para verificar cada etapa de seu trabalho. O resultado? Eles provaram que, para esses loops ímpares específicos, a velocidade máxima de comunicação perfeita é maior do que qualquer um havia calculado anteriormente.

O Jogo dos Cruzamentos Seguros

Vamos decompor o que os autores realmente fizeram. Eles estavam olhando para grafos que parecem anéis simples com um número ímpar de pontos: um anel de 7, um anel de 11, um anel de 13, e assim por diante. Por muito tempo, os matemáticos souberam o "limite de velocidade" (a capacidade de Shannon) para um anel de 5 pontos. Mas para anéis com 7 pontos ou mais, a resposta ficou estagnada em uma névoa. Sabíamos que era pelo menos um certo número, mas não sabíamos se poderia ser maior.

Os autores usaram um método que parece uma receita mágica para cultivar seu grupo seguro. Imagine que você tem um pequeno clube seguro de amigos (um conjunto de pontos) em um único mapa. O artigo descreve um "teorema de produto", que é como uma máquina que pega dois desses mapas e os esmaga juntos para criar um novo mapa, maior. Se você tem um clube seguro no primeiro mapa e um clube seguro no segundo mapa, você pode combiná-los para criar um clube seguro no novo mapa maior. Normalmente, o tamanho deste novo clube é apenas o tamanho do primeiro clube multiplicado pelo tamanho do segundo. Mas os autores encontraram um "gadget" ou truque especial. Ao usar um padrão específico de conexões (chamado de "tupla válida"), eles puderam tornar o novo clube maior do que a multiplicação simples sugeriria.

Pense nisso como: Se você tem uma equipe de 2 pessoas que podem trabalhar juntas sem brigar, e você combina duas dessas equipes, você pode esperar uma equipe de 4 pessoas. Mas com este truque especial, os autores descobriram uma maneira de combinar essas equipes e obter uma equipe de 5 pessoas que se dão perfeitamente bem. Ao repetir este truque repetidamente, empilhando os mapas cada vez mais alto, eles puderam transformar esses grupos seguros em grupos massivos.

Os Novos Recordes

A equipe aplicou esta receita a sete anéis ímpares diferentes: aqueles com 7, 11, 13, 15, 19, 21 e 23 pontos. Para cada um, eles começaram com um grupo seguro conhecido e rodaram sua máquina de "empilhamento" muitas vezes. O resultado foi um novo limite inferior para a capacidade de Shannon.

Aqui está o que eles descobriram, com os números exatamente como calcularam:

Para o anel de 7 pontos, eles provaram que a capacidade é pelo menos 3.258805369885. Isso é um pouco acima da melhor estimativa anterior.
Para o anel de 11 pontos, o novo piso é 5.294502522149.
Para o anel de 13 pontos, eles elevaram o limite para 6.302455083464.
Para o anel de 15 pontos, o número é 7.301600534487.
Para o anel de 19 pontos, eles alcançaram 9.357192705918.

Para o anel de 21 pontos, o limite é 10.342455853338.

E para o anel de 23 pontos, eles encontraram uma capacidade de pelo menos 11.328224257774.

Esses números podem parecer uma sequência de dígitos aleatórios, mas no mundo da teoria da informação, eles representam uma melhoria concreta. Significa que, para essas redes específicas, agora sabemos com certeza que podemos enviar mensagens um pouco mais rápido do que pensávamos ser possível antes.

O Árbitro Digital

O que torna este artigo especial não são apenas os números, mas como eles os obtiveram. A matemática envolvida é incrivelmente complexa, envolvendo enormes conjuntos de dados e milhares de etapas. É o tipo de trabalho onde um humano poderia facilmente perder um erro minúsculo. Para resolver isso, os autores escreveram toda a sua prova em uma linguagem de computador chamada Lean.

Pense no Lean como um árbitro digital hiper rigoroso que não aceita um "eu acho que está certo" ou "parece bom para mim". Ele exige uma prova lógica absoluta para cada etapa. Se os autores cometessem um erro em sua lógica, o Lean pararia e diria: "Não, isso não segue". O fato de o artigo ser "verificado pelo Lean" significa que um computador verificou cada linha de seu raciocínio e confirmou que seus novos limites são matematicamente sólidos. Eles não apenas simularam os resultados; eles provaram formalmente.

Os autores também mencionam que usaram modelos de linguagem de grande escala (como chatbots de IA avançados) para ajudá-los a encontrar os padrões iniciais e as receitas para esses grupos seguros. É um pouco como ter um assistente criativo que sugere uma ideia selvagem, e então os matemáticos usam suas ferramentas rigorosas para testar se essa ideia realmente se sustenta. Neste caso, a IA sugeriu um caminho, e a equipe humano-matemático-IA percorreu todo o caminho até uma linha de chegada verificada.

Por Que Isso Importa

Você pode se perguntar: "E daí? Só sabemos que o número é um pouco maior". A resposta reside na natureza do problema. Por décadas, a capacidade desses anéis ímpares tem sido uma questão aberta. Sabíamos que a resposta estava em algum lugar entre um limite inferior e um limite superior (o limite de Lovász), mas não conseguíamos defini-la. Cada vez que elevamos o limite inferior, mesmo que por uma fração minúscula, estreitamos a lacuna. Estamos chegando mais perto da resposta verdadeira.

Este trabalho mostra que, mesmo para problemas que estão travados há muito tempo, ainda há espaço para melhoria se você tiver as ferramentas certas e a paciência para verificar seu trabalho com os padrões mais rigorosos possíveis. Os autores não resolveram todo o mistério da capacidade de Shannon para todos os anéis ímpares, mas eles limparam alguns cantos nebulosos, provando que, para anéis de 7, 11, 13, 15, 19, 21 e 23, podemos nos comunicar um pouco mais rápido do que acreditávamos anteriormente.

Resumo Técnico: Limites Inferiores Verificados em Lean para a Capacidade de Shannon de Ciclos Ímpares

Enunciado do Problema
O artigo aborda o problema de longa data de determinar a capacidade de Shannon, $\Theta(G)$ , para ciclos ímpares $C_n$ onde $n \geq 7$ . A capacidade de Shannon é definida como $\Theta(G) := \sup_{d \geq 1} \alpha(G^{\boxtimes d})^{1/d}$ , onde $\alpha$ denota o número de independência e $\boxtimes$ denota o produto forte de grafos. Enquanto Lovász determinou que $\Theta(C_5) = \sqrt{5}$ usando a função theta $\vartheta(G)$ , as capacidades exatas para todos os ciclos ímpares de comprimento sete ou maior permanecem desconhecidas. O principal desafio reside em encontrar conjuntos independentes maiores em potências fortes superiores desses ciclos para melhorar os limites inferiores conhecidos.

Metodologia
Os autores empregam um procedimento iterativo baseado em uma "construção de gadget" e um "lema de produto" proposto recentemente por Gao (2026), que por sua vez baseia-se em métodos de Itty, Rosin, Carstensen e Reichman (2026). O núcleo da metodologia envolve:

Tuplas Válidas: Para um grafo $G$ , uma tupla válida $\tau = (I, S, f_0, f_1, X)$ é definida, onde $I$ é um conjunto independente, $S \subseteq I$ , e $f_0, f_1$ são mapeamentos específicos satisfazendo restrições de vizinhança estritas. Essa tupla gera um "perfil" $\Pi(\tau) = (|I|, |S|, |X|, |X \setminus (N_G[f_0(S)] \cup N_G[f_1(S)])|)$ .
Operação de Produto: Uma operação binária $\star$ é definida sobre perfis. O Teorema 1 estabelece que, se $\tau$ e $\tau'$ são tuplas válidas para os grafos $G$ e $H$ , existe uma tupla válida para o produto forte $G \boxtimes H$ cujo perfil é o produto $\star$ dos perfis individuais.
Construção Iterativa: Partindo de uma tupla válida descoberta computacionalmente em uma potência específica de um ciclo ímpar, os autores aplicam iterativamente o produto $\star$ para gerar perfis para potências superiores. Este processo constrói conjuntos independentes em potências fortes $C_n^{\boxtimes d}$ que são maiores do que os obtidos por simples produtos cartesianos dos conjuntos independentes de base.
Verificação Formal: Um componente crítico da metodologia é a formalização completa desses limites no assistente de prova Lean. As tuplas de base (conjuntos $I, S, X$ e mapeamentos $f_0, f_1$ ) são codificadas como literais explícitos, e sua validade é verificada mecanicamente dentro do ambiente Lean.

Contribuições Principais e Resultados
O artigo apresenta novos limites inferiores melhorados para as capacidades de Shannon de sete pequenos ciclos ímpares ( $C_7, C_{11}, C_{13}, C_{15}, C_{19}, C_{21}, C_{23}$ ). Esses limites são derivados da identificação de tuplas de base válidas específicas e da aplicação do procedimento de produto iterativo. Os resultados são:

$\Theta(C_7)$ : Melhorado para $\geq 3.258805369885\dots$ (anteriormente $3.2587891\dots$ por Gao 2026). A construção utiliza uma tupla de base em $C_7^{\boxtimes 5}$ iterada até a potência 200.
$\Theta(C_{11})$ : Melhorado para $\geq 5.294502522149\dots$ (anteriormente $5.2897736\dots$ por Itty et al. 2026). A tupla de base está em $C_{11}^{\boxtimes 3}$ , iterada até a potência 174.
$\Theta(C_{13})$ : Melhorado para $\geq 6.302455083464\dots$ (anteriormente $6.3001091\dots$ por Itty et al. 2026). A tuola de base está em $C_{13}^{\boxtimes 6}$ , iterada até a potência 432.
$\Theta(C_{15})$ : Melhorado para $\geq 7.301600534487\dots$ (anteriormente $7.3013990\dots$ por Itty et al. 2026). A tupla de base está em $C_{15}^{\boxtimes 4}$ , iterada até a potência 4096.
$\Theta(C_{19})$ : Melhorado para $\geq 9.357192705918\dots$ (anteriormente $9.3571200\dots$ por Baumert et al. 1971). A tupla de base está em $C_{19}^{\boxtimes 4}$ , iterada até a potência 16384.
$\Theta(C_{21})$ : Melhorado para $\geq 10.342455853338\dots$ (anteriormente $10.3422729\dots$ por Baumert et al. 1971). A tupla de base está em $C_{21}^{\boxtimes 4}$ , iterada até a potência 4096.
$\Theta(C_{23})$ : Melhorado para $\geq 11.328224257774\dots$ (anteriormente $11.3278379\dots$ por Baumert et al. 1971). A tupla de base está em $C_{23}^{\boxtox 4}$ , iterada até a potência 2048.

As melhorias, embora numericamente pequenas (variando de $10^{-5}$ a $10^{-3}$ ), representam o estado da arte atual para esses ciclos específicos.

Significância e Alegações
O artigo alega significância primariamente através da verificação rigorosa desses resultados. Ao formalizar toda a construção e os limites resultantes em Lean, os autores garantem que os complexos argumentos combinatórios e as construções de conjuntos específicas estejam livres de erro humano. O trabalho segue a trajetória de pesquisas recentes utilizando modelos de linguagem de grande escala (LLMs) para descobrir construções iniciais (como visto em [IRCR26] e [Gao26]), mas distingue-se ao fornecer uma prova totalmente formalizada e verificada por máquina da validade das tuplas de base e da correção da aplicação do teorema de produto iterativo. Os autores não alegam ter resolvido o problema geral da capacidade de Shannon para ciclos ímpares, nem propõem novos arcabouços teóricos além da aplicação do lema de produto existente de Gao; em vez disso, fornecem os melhores limites inferiores numéricos conhecidos atualmente para essas instâncias específicas, verificados com certeza matemática.

O Jogo dos Cruzamentos Seguros

Os Novos Recordes

O Árbitro Digital

Por Que Isso Importa

Mais como este