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

Resumo Técnico: Uma Prova de $K_8(4,2) = 23$ Certificada em Lean

Enunciado do Problema
O artigo aborda a determinação do número de cobertura exato $K_q(n,r)$, definido como o tamanho mínimo de um código de cobertura de raio-$r$ no espaço de Hamming $q$-ário de comprimento $n$. Especificamente, ele resolve o valor para o caso octonário com comprimento 4 e raio 2: $K_8(4,2)$. Antes deste trabalho, os intervalos existentes (especificamente as tabelas de Kéri) situavam este valor no intervalo $[22, 23]$. O limite inferior foi derivado do limite de domínio de rook de Rodemich, enquanto o limite superior foi sustentado por limites de alfabetos grandes. O objetivo era fechar este intervalo provando o limite inferior $K_8(4,2) \ge 23$.

Metodologia
A prova é formalizada no provador de teoremas Lean 4 utilizando a biblioteca mathlib. Ela emprega uma abordagem de "prova portadora" (proof-carrying) onde o resultado é estabelecido via dois certificados independentes: um limite superior explícito e um limite inferior estrutural.

1. Limite Superior ($K_8(4,2) \le 23$):
   Os autores fornecem um código explícito consistindo de 23 palavras em $(\text{Fin } 8)^4$. A prova formal verifica duas condições: a cardinalidade do conjunto é no máximo 23, e cada palavra no espaço ambiente (4096 palavras) está a uma distância de Hamming de no máximo 2 de pelo menos uma palavra do código. Esta é uma verificação finita exaustiva.

2. Limite Inferior ($K_8(4,2) \ge 23$):
   O núcleo do artigo é um argumento de não existência estrutural para qualquer cobertura hipotética $C^*$ com $|C^*| \le 22$. A prova procede através de uma sequência de reduções:

   • Contagem de Fibras: Para uma cobertura hipotética, os autores definem "fibras" $C^*_{i,a}$ (palavras com o símbolo $a$ na coordenada $i$). Eles provam que cada fibra deve conter pelo menos duas palavras. Isso estabelece uma base de 16 palavras ($8 \text{ símbolos} \times 2$) por coordenada, deixando um "orçamento" de no máximo 6 palavras excedentes para o caso $|C^*|=22$ (ou 5 para $|C^*| \le 21$).
   • Grafos de Pares Ausentes: A prova muda para um ponto de vista "inverso", analisando quais pares de símbolos estão ausentes das projeções do código sobre pares de coordenadas. Esses pares ausentes formam grafos $E_{ij}$.
   • Caso $|C^*| \le 21$: Usando o pequeno orçamento de excesso, os autores demonstram via contagem combinatória que os grafos de pares ausentes devem conter um "clique quadripartido simultâneo" (um conjunto de quatro símbolos $a,b,c,d$ tal que todos os seis pares de coordenadas estão ausentes). O Lema 7 prova que tal clique não pode existir em uma cobertura válida de raio-2, eliminando assim coberturas de tamanho 21 ou inferior.
   • Caso $|C^*| = 22$: Para o caso restante, a prova reduz o problema a uma classificação finita do "perfil" dos grafos de pares ausentes. Os autores mostram que qualquer perfil válido deve exibir uma estrutura específica de "bloco comum $3+3+2$".
   • Integração SAT/LRAT: A classificação desses perfis é grande demais para enumeração manual. Os autores codificam as restrições (limites de grau de linha/coluna e a condição de não-clique) em instâncias de Forma Normal Conjuntiva (CNF). Eles utilizam um solver SAT não confiável para gerar refutações de Linear RAT (LRAT) (provas de insatisfatibilidade).
   • Verificação Formal: O Lean analisa esses certificados LRAT e reproduz mecanicamente as refutações para provar que nenhum perfil válido existe para uma cobertura de 22 palavras.
   • Contradição Final: Mesmo que uma estrutura de bloco comum fosse assumida, os autores derivam uma contradição no "componente de 2 símbolos" da estrutura. Este componente exigiria um array binário de força-2 de comprimento 4 com no máximo 4 linhas, o que é matematicamente impossível.

Principais Contribuições

• Valor Exato: O artigo estabelece o valor exato $K_8(4,2) = 23$, fechando o intervalo anteriormente conhecido de $[22, 23]$.
• Limite Inferior Formalizado: Fornece uma prova totalmente formalizada em Lean 4 que exclui todas as coberturas de 22 palavras. Isso é alcançado não por argumentos de volume, mas por obstruções estruturais derivadas de contagens de fibras e grafos de pares ausentes.
• Artefato de Prova Portadora: O resultado é empacotado como um artefato Lean contendo o código explícito, os lemas estruturais, as instâncias CNF e as refutações LRAT. Crucialmente, o solver SAT não faz parte da base de computação confiável; o Lean verifica os certificados LRAT internamente.
• Padrão para Limites Computacionais: O artigo introduz um padrão reutilizável para anexar evidência produzida por solver a limites de códigos de cobertura. Ele separa a "descoberta" (solver não confiável) da "verificação" (kernel confiável de Lean), permitindo que grandes problemas de classificação finita sejam resolvidos computacionalmente enquanto mantém a correção formal.

Resultados
O resultado primário é o teorema $K_8(4,2) = 23$.

• Limite Superior: Provado por um código explícito de 23 palavras.
• Limite Inferior: Provado ao mostrar que uma cobertura de tamanho 22 leva a uma contradição via um "sistema de bloco comum $3+3+2$" forçado, que implica a existência de um array binário impossível.
• Desempenho: A verificação formal envolve recursos computacionais significativos. A reprodução em modo kernel do arquivo de prova principal exigiu aproximadamente 143 GiB de RAM, enquanto o modo nativo reduziu isso para cerca de 5,5 GiB. A fase de verificação de LRAT levou aproximadamente 17 minutos em modo kernel.

Significância e Alegações
O artigo alega significância principalmente no campo da matemática formalizada e da metodologia de combinar raciocínio combinatório com certificados computacionais.

• Mudança Metodológica: Demonstra que a combinatória estrutural pode ser combinada com evidência computacional de "prova portadora". O solver SAT é usado para descobrir obstruções finitas, mas a ponte matemática e a verificação da saída do solver são tratadas inteiramente dentro do provador de teoremas.
• Fronteira de Confiança: O trabalho esclarece a fronteira de confiança em provas formais envolvendo solvers SAT. O solver é não confiável; o kernel do Lean verifica os certificados LRAT e a dedução lógica que conecta esses certificados à afirmação do código de cobertura.
• Escalabilidade: O resultado serve como um caso de teste para lidar com problemas de códigos de cobertura que são grandes demais para prova manual, mas pequenos o suficiente para serem reduzidos a problemas de classificação finos solucionáveis por solvers SAT.
• Sem Novas Aplicações: O artigo não alega novas aplicações para o valor $K_8(4,2)=23$ em si, nem propõe novos protocolos experimentais. Sua contribuição é estritamente a resolução de um problema específico aberto em tabelas de códigos de cobertura e a demonstração de um fluxo de trabalho de verificação formal para tais problemas.