Pular para o conteúdo
Matemática
Índice

§ Entenda o problema

Cobrir tudo com o mínimo.

A mesma pergunta, em quatro profundidades. Escolha a sua.

Antenas num bairro de palavras

Quantas antenas, no mínimo, garantem que toda casa fique a no máximo R quarteirões de uma delas? Kq(n,R) é esse número mínimo, só que as “casas” são palavras e a distância é contar letras diferentes.

AnalogiaAntenas de celular: cada uma cobre uma vizinhança; queremos cobrir a cidade inteira gastando o mínimo.

ExemploCom palavras de 3 bits e alcance 1, duas antenas bastam: 000 e 111. Teste no cubo ao lado.

Com JavaScript, este cubo é interativo: clique numa palavra para ver a sua esfera de raio 1.

A cota da esfera: nenhum código cobre com menos palavras que

Kq(n,R) ≥ qn ∑i=0R(ni)(q−1)i

Para K7(6,4): 117.649 ÷ 24.337 ≈ 4,8, logo pelo menos 5. A verdade é 14: a distância entre esse piso e o valor real é onde mora o trabalho.

Glossário
Palavra
Sequência de n símbolos tirados de um alfabeto com q símbolos.
Distância de Hamming
Número de posições em que duas palavras diferem.
Esfera de raio R
Todas as palavras a distância ≤ R de um centro.
Código de cobertura
Conjunto de palavras cujas esferas de raio R contêm todas as palavras.
Kq(n,R)
Tamanho mínimo de um código de cobertura.
Cota superior / inferior
Prova de que K ≤ M (exibindo um código) ou de que K ≥ M (mostrando que nada menor cobre).
Célula exata
Quando as duas cotas coincidem: o valor está determinado.
Kernel do Lean
O núcleo pequeno do assistente de provas Lean 4, que confere cada passo de uma demonstração.

I. Manifesto

Toda descoberta cara deve virar verificação barata.

Entropia local é a incerteza de um trabalho que ainda depende de alguém lembrar. Reverter isso custa energia: alguém gasta computação cara e descobre alguma coisa. O ponto não é evitar o custo, é fazer com que ele produza um objeto que barateia a próxima vez.

Em códigos de cobertura isso tem forma exata. Achar um código pequeno que cobre todo o espaço é busca; conferir que ele cobre é contar. Provar que nenhum código menor existe é busca maior ainda; conferir o certificado é rodar um verificador, ou o kernel do Lean.

Este repositório guarda cada cota com a sua procedência e o seu estado. Nada sobe de estado por opinião: sobe porque um verificador independente, ou uma prova formal, passou.

  • caos estrutura
  • implícito explícito
  • ambiguidade métrica
  • descoberta verificação

II. Princípios

Os axiomas do ofício.

  1. Meça antes de afirmar

    Frase sem número é hipótese. A conclusão nunca sai mais larga que a evidência.

  2. Enviado não é entregue

    Ausência de erro não prova nada. Prova-se pelo estado depois: o certificado conferido, o teorema compilado.

  3. Procedência ou nada

    Todo número tem fonte, versão e estado. Cota sem origem não entra no ledger.

  4. O que você mediu vence o que você leu

    Literatura é ponto de partida; a cota sobe de estado quando é reproduzida aqui.

  5. Engenheiro torna regras determinísticas

    Regra que mora na cabeça de alguém é entropia; regra que mora num teste, não é.

  6. Lacuna declarada vale mais que acerto imaginado

    O que ainda não foi conferido é dito em voz alta, com o nome do estado.

III. Cotas de Kéri

Quantas esferas cobrem o espaço?

Kq(n,R) = o menor código em ℤqn cujas esferas de Hamming de raio R cobrem tudo.

As tabelas de Gerzson Kéri reúnem, para cada alfabeto q, comprimento n e raio R, a melhor cota inferior e superior conhecidas. Cada célula com intervalo aberto é uma pergunta: existe um código menor, ou dá para provar que não existe?

É o terreno ideal para o método: encontrar um código é caro, conferir que ele cobre é barato e exato. Fechar uma célula é transformar uma faixa de incerteza num número — e deixar a prova onde qualquer um pode conferir.

  1. K3(6,2)15–17= 17Potencialmente novoinferior · CERTIFICATE_VERIFIEDsuperior · INDEPENDENTLY_REPRODUCED
  2. K7(6,4)13–15= 14Potencialmente novoinferior · CERTIFICATE_VERIFIEDsuperior · INDEPENDENTLY_REPRODUCED
  3. K7(5,3)15–17= 17Potencialmente novoinferior · CERTIFICATE_VERIFIEDsuperior · CLAIMED
  4. K7(4,2)17–19= 19inferior · FORMALIZEDsuperior · FORMALIZED
  5. K7(9,4)≤ 1475≤ 1134inferior · CLAIMEDsuperior · INDEPENDENTLY_REPRODUCED

“Potencialmente novo”: não encontrado na literatura que pesquisamos (docs/exatos/NOVIDADE_V09.md). Em K7(5,3), a cota superior 17 ganhou código próprio de 17 palavras e teorema Lean; a inferior é certificado verificado fora do Lean.

IV. Números ao vivo

O ledger, contado.

A machine-checked ledger of covering-code upper bounds, with formally certified exact entries. A tabela inteira não foi verificada formalmente: cada cota tem o seu estado, e a maioria das cotas inferiores ainda é herdada da literatura.

1145
células Kq(n,R) no ledger
523
exatas: cota inferior igual à superior
622
ainda abertas
488
cotas superiores no Lean (FORMALIZED ou acima)
Cotas superiores, por estado1145 cotas
  • CLAIMED · 657
  • FORMALIZED · 435
  • INDEPENDENTLY_REPRODUCED · 53

Cotas inferiores: 1140 CLAIMED, 3 CERTIFICATE_VERIFIED, 2 FORMALIZED.

Números embutidos na página (ledger/COBERTURA.md, v0.9.1).

V. O teorema do James

A filosofia, compilada.

Os três pilares da filosofia do James — conhecimento, segurança e alma — provados em Lean 4, sem Mathlib e sem sorry. Escrever as provas foi busca; conferi-las é o kernel, em milissegundos.

Amortização

Partindo de base vazia, o número de buscas é exatamente o número de tarefas distintas; se elas crescem mais devagar que as tarefas, o custo por tarefa tende ao custo de verificar.

Conhecimento.lean

Gate

Para qualquer log de eventos, inclusive adversário, nenhuma ação crítica aparece executada sem aprovação registrada.

Seguranca.lean

Replay, retomada, revezamento

O estado é função do log, não do host: um corpo pode morrer em qualquer evento e outro retoma do snapshot.

Alma.lean

Fronteira. Os teoremas valem para os modelos definidos lá, não para o código de produção: se o sistema se comporta como o modelo, então as propriedades valem.

VI. Horizonte

Os sete Problemas do Milênio.

Em 2000, o Clay Mathematics Institute escolheu sete problemas e ofereceu US$ 1 milhão por cada solução. Um foi resolvido; seis seguem abertos.

  • P versus NP

    Todo problema cuja solução se verifica depressa também se resolve depressa?

    Aberto

  • Hipótese de Riemann

    Todos os zeros não triviais da função zeta de Riemann têm parte real 1/2.

    Aberto

  • Yang–Mills e a lacuna de massa

    Existe uma teoria quântica de Yang–Mills em ℝ4 com lacuna de massa positiva?

    Aberto

  • Navier–Stokes

    As equações em três dimensões têm sempre soluções suaves e globais a partir de dados iniciais suaves?

    Aberto

  • Conjectura de Hodge

    Em variedades algébricas projetivas, as classes de Hodge são combinações racionais de classes de subvariedades algébricas.

    Aberto

  • Birch e Swinnerton-Dyer

    O posto de uma curva elíptica sobre os racionais é a ordem do zero da sua função L em s = 1.

    Aberto

  • Conjectura de Poincaré

    Toda 3-variedade fechada e simplesmente conexa é homeomorfa à 3-esfera. Provada por Grigori Perelman (2002–2003); ele recusou o prêmio do Clay, concedido em 2010.

    Resolvido

Não resolvemos nem atacamos nenhum destes problemas. Eles aparecem aqui como horizonte e inspiração do método: perguntas em que descobrir e verificar parecem viver em escalas diferentes. Fonte do status: claymath.org.

VII. A escada

Contra o não-provado, uma escada de estados.

Cada cota começa como afirmação e só sobe um degrau quando um instrumento mais exigente confere. Os estados são cumulativos.

  1. INDEPENDENTLY_REPRODUCED

    No Lean e reproduzida por um segundo caminho independente.

    53cotas
  2. FORMALIZED

    Teorema aceito pelo kernel do Lean 4.

    435cotas
  3. CERTIFICATE_VERIFIED

    Certificado conferido por verificador (estado típico de cota inferior).

    0cotas
  4. WITNESS_CHECKED

    Código explícito conferido por programa.

    0cotas
  5. CLAIMED

    Afirmada na literatura; nada conferido aqui.

    657cotas
  1. DefinirFixar a célula Kq(n,R) e a melhor cota publicada, com fonte.
  2. BuscarGastar computação cara: busca local, programação inteira, SAT, simetria.
  3. CertificarTransformar o achado em objeto conferível: um código explícito ou um certificado de inexistência.
  4. VerificarConferir com um verificador independente e, quando cabe, com o kernel do Lean.
  5. RegistrarSubir o estado no ledger, com hash, versão e a lacuna que restar.

VIII. Lacunas honestas

O que ainda não está provado.

  • As cotas inferiores novas (K3(6,2) ≥ 17, K7(6,4) ≥ 14, K7(5,3) ≥ 16) estão fora do Lean: são certificados conferidos por verificador (CERTIFICATE_VERIFIED), não teoremas do kernel.
  • “Potencialmente novo” quer dizer: não encontrado na literatura que pesquisamos. Não é prova de prioridade.
  • Quase todas as cotas inferiores do ledger são herdadas da literatura (CLAIMED), e a maior parte das cotas superiores também.
  • Os teoremas do James valem para modelos; ancorá-los no código real é trabalho em aberto.

IX. Links e citação

Confira você mesmo.

@software{patzdorf_matematica,
  author  = {Patzdorf, Thiago},
  title   = {Covering codes checked by the Lean kernel},
  year    = {2026},
  version = {0.9.1},
  doi     = {10.5281/zenodo.23085769},
  url     = {https://github.com/thiagopatzdorf/Matematica}
}