🔢 mathematics

Kernel-Checked Exclusions for the Erdős-Selfridge Odd Covering Problem: Any Odd Covering of ℤ Has lcm Exceeding 10000

Este artigo apresenta uma formalização em Lean 4 totalmente verificada pelo kernel, provando que qualquer cobertura finita dos inteiros por módulos ímpares distintos maiores que 1 deve ter um mínimo múltiplo comum superior a 10.000, estabelecendo assim uma exclusão mecanicamente certificada para o problema da cobertura ímpar de Erdős-Selfridge sem depender de resolvedores computacionais não verificados.

Autores originais: Ibrahim Mian, Shayaan Siddique

Publicado 2026-07-29✓ Author reviewed ⓘ

📖 7 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Ibrahim Mian, Shayaan Siddique

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 pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine os números inteiros (os números inteiros como 1, 2, 3 e assim por diante) como uma rodovia infinita que se estende em ambas as direções. No mundo da matemática, existe um quebra-cabeça fascinante sobre "cobrir" esta rodovia. Um sistema de cobertura é como uma equipe de guardas de segurança, cada um estacionado em um local específico e designado para um padrão de patrulha. Por exemplo, um guarda pode verificar cada 2ª casa, outro cada 3ª casa e um terceiro cada 4ª casa. Se você os alinhar da maneira certa, suas rotas de patrulha se sobrepõem de tal forma que cada uma das casas na rodovia infinita é visitada por pelo menos um guarda. Os matemáticos sabem há décadas que é possível fazer isso, mas há um detalhe: em todos os exemplos conhecidos, pelo menos um dos guardas tem um padrão de patrulha "par" (como verificar cada 2ª ou 4ª casa).

Isso leva a uma questão persistente que assombra os matemáticos há mais de 70 anos: é possível cobrir toda a rodovia usando apenas guardas com padrões de patrulha "ímpares" (como cada 3ª, 5ª ou 7ª casa), onde nenhum dois guardas tenham o mesmo tamanho de padrão? Isso é conhecido como o problema da cobertura ímpar de Erdős–Selfridge. É um pouco como perguntar se você pode revestir um chão usando apenas azulejos de formatos ímpares sem nunca usar um único azulejo de formato par. Embora não saibamos a resposta final, este novo artigo atua como um inspetor superpreciso e à prova de robôs. Ele não resolve todo o mistério, mas prova com absoluta certeza que, se tal sistema de cobertura ímpar existir, os números envolvidos devem ser incrivelmente grandes — muito maiores do que qualquer pessoa fora a ser descartado anteriormente com um computador que não comete erros.

A Descoberta do Artigo: Uma Zona de Exclusão à Prova de Robôs

Este artigo, escrito por Ibrahim Mian e Shayaan Siddique, não afirma ter encontrado a solução para o problema da cobertura ímpar. Em vez disso, ele constrói uma "fortaleza digital" para provar que qualquer solução potencial deve ser muito maior que 10.000. Pense no problema como um cadeado gigante com uma combinação feita de números. Os autores queriam saber: "A combinação poderia ser pequena, como 945 ou 1.200?" A resposta deles é um "Não" definitivo, mas com um toque muito especial: eles não usaram apenas uma calculadora; eles usaram um robô matemático (um programa de computador chamado Lean 4) para verificar cada passo de sua lógica, garantindo que nenhum erro humano ou suposição oculta escapasse.

Aqui está como eles fizeram isso, usando algumas metáforas criativas:

1. A Armadilha da Densidade (A Contagem da Multidão)
Primeiro, os autores observaram a "densidade" dos guardas. Se você tiver um grupo de guardas com diferentes tamanhos de patrulha ímpares, você pode calcular quanto da rodovia eles cobrem. Para que eles cubram tudo, a cobertura combinada deve somar 100%. A matemática mostra que, para isso acontecer com números ímpares, o "mínimo múltiplo comum" (MMC) — que é como o comprimento total do padrão repetitivo antes de recomeçar — deve ser um tipo especial de número chamado "abundante". Um número abundante é aquele onde a soma de seus divisores (os números que o dividem exatamente) é maior que o próprio número. É como um número que é tão popular que seus amigos somam mais do que ele próprio vale.

2. O Teste do Chão (A Barreira de 945)
Os autores provaram que o menor número ímpar que é "abundante" é 945. Isso significa que, se um sistema de cobertura totalmente ímpar existir, seu comprimento de padrão deve ser pelo menos 945. Algo menor que isso é matematicamente impossível. Este foi o primeiro degrau de sua escada, um fato que eles verificaram com uma checagem de computador que levou cerca de 80 segundos de cálculo puro e inabalável.

3. Os Certificados de Capacidade (O Teste de Sobreposição)
É aqui que a magia acontece. Saber apenas que os números são "abundantes" não é suficiente; você também tem que verificar se os guardas realmente se encaixam sem deixar lacunas. Os autores criaram "certificados de capacidade". Imagine tentar encaixar um conjunto de peças de quebra-cabeça em uma caixa. Mesmo que as peças pareçam que deveriam caber, às vezes elas se sobrepõem demais ou deixam pequenos buracos. Os autores escreveram um teste específico para cada número ímpar abundante abaixo de 10.000. Eles perguntaram: "Se tentarmos construir um sistema de cobertura usando esses números ímpares específicos, as lacunas entre os guardas tornam-se grandes demais para preencher?"

Para cada um dos números ímpares abundantes abaixo de 10.000 (existem exatamente 23 deles), o teste disse "Não, é impossível". As lacunas eram grandes demais, ou as sobreposições eram bagunçadas demais. O computador verificou isso para todos os 23 números, provando que nenhum deles poderia ser a combinação secreta.

4. O Veredito Final (O Limite de 10.000)
Ao combinar esses passos, os autores provaram um teorema principal: Qualquer sistema de cobertura dos inteiros usando módulos ímpares distintos maiores que 1 deve ter um mínimo múltiplo comum (MMC) maior que 10.000.

Em termos mais simples: Se alguém afirma ter encontrado uma maneira de cobrir a rodovia infinita usando apenas padrões de patrulha de números ímpares, essa pessoa está mentindo se o seu padrão se repetir a cada 10.000 passos ou menos. O padrão deve ser mais longo que isso.

Por Que Isso Importa (Mesmo Que Não Seja a Resposta Final)

Você pode se perguntar: "E daí? Eles apenas provaram que o número tem que ser maior que 10.000. Nós já sabíamos que era difícil". Os autores são muito honestos sobre isso: eles não resolveram o problema inteiro. A resposta real pode ser um número como 100.000 ou um bilhão. No entanto, a maneira como eles fizeram isso é o verdadeiro avanço.

Normalmente, quando matemáticos usam computadores para verificar listas enormes de números, eles dependem de softwares de "caixa preta" que podem conter erros ou suposições ocultas. Este artigo é diferente. Eles construíram todo o seu argumento dentro de um "kernel de prova" — um núcleo minúsculo e confiável de um programa de computador que verifica cada passo lógico como um contador paranoico. Eles não usaram nenhum "atalho mágico" ou código não verificado. Eles até provaram que seu código de computador funciona corretamente testando-o contra exemplos conhecidos (como o clássico sistema de cobertura de 12 passos) para garantir que não dissesse "impossível" quando algo era, na verdade, possível.

Eles também criaram uma ponte que conecta o mundo infinito de todos os inteiros ao mundo finito das verificações de computador. Isso significa que, no futuro, se alguém realizar uma busca em um supercomputador para encontrar uma solução, este artigo fornece uma maneira de verificar os resultados sem confiar cegamente no computador.

A Conclusão

O artigo descarta a possibilidade de um sistema de cobertura ímpar "pequeno". Ele diz: "Se a resposta existe, ela está escondida em algum lugar além de 10.000". Ele não nos diz onde a resposta está, mas limpou todo o bairro de números abaixo de 10.000 com um nível de certeza que nenhum ser humano poderia alcançar sozinho. É um "Não" rigoroso e verificado por robôs para os números pequenos, deixando o mistério aberto para os números grandes, mas com uma nova ferramenta inabalável para verificar futuras descobertas.

Resumo Técnico: Exclusões Verificadas pelo Kernel para o Problema de Cobertura Ímpar de Erdős–Selfridge

Enunciado do Problema
O artigo aborda o problema da cobertura ímpar de Erdős–Selfridge (problema nº 7 de Erdős), que questiona se existe um sistema de cobertura dos inteiros $\mathbb{Z}$ onde todos os módulos são ímpares, distintos e maiores que 1. Um sistema de cobertura é uma família finita de classes de congruência $a_i \pmod{n_i}$ cuja união é $\mathbb{Z}$ . Embora se saiba que todo sistema de cobertura existente com módulos distintos $>1$ contém pelo menos um módulo par, a existência de uma variante puramente ímpar permanece um problema em aberto.

Metodologia
Os autores apresentam uma formalização em Lean 4 (usando mathlib) que estabelece uma exclusão verificada pelo kernel: qualquer cobertura de $\mathbb{Z}$ por módulos ímpares distintos $>1$ deve ter um mínimo múltiplo comum (mmc) dos módulos superior a 10.000. A estratégia de prova evita computação não verificada ou solvers externos, baseando-se em uma cadeia de cinco etapas formalizadas:

Argumento de Densidade: Os autores formalizam o argumento clássico do folclore de que, se um sistema de cobertura utiliza módulos distintos que dividem $N$ (todos $>1$ ), a soma de seus recíprocos deve ser pelo menos 1. Isso implica que $2N \le \sigma_1(N)$ , significando que $N$ deve ser perfeito ou abundante.
Redução ao MMC: Para qualquer cobertura de $\mathbb{Z}$ , a prova reduz o problema ao mmc ( $L$ ) dos módulos. Como os módulos são distintos e ímpares, $L$ deve ser um número ímpar, não deficiente (perfeito ou abundante).
Piso de Abundância: Uma computação verificada pelo kernel confirma que o menor número abundante ímpar é 945. Consequentemente, qualquer tal cobertura deve ter um mmc $\ge 945$ .
Certificados de Capacidade: Para excluir candidatos específicos, os autores formalizam um limite de "capacidade de Resto Chinês". Esta desigualdade aritmética decidível contabiliza as sobreposições entre classes de congruência com módulos mutuamente primos. Se os pontos "não cobertos" restantes após considerar essas sobreposens não puderem ser cobertos pelos divisores restantes de $N$ $N$ , o sistema é provado impossível.
- Um "lema de relaxação monotônica" garante que um certificado derivado de uma família de coprimalidade total se aplica mesmo se um sistema de cobertura utilizar apenas um subconjunto desses módulos.
- Esta etapa gera um certificado para cada um dos 23 números abundantes ímpares abaixo de 10.000, refutando-os como potenciais valores de mmc para $N$ .
Enumeração: Um avaliador de soma de divisores com combustível constante (sigma100) é implementado para evitar a ineficiência de mecanismos de divisão genéricos na redução do kernel. Isso permite que o kernel verifique que os 23 números abundantes ímpares abaixo de 10.000 são os únicos candidatos nesse intervalo.

Principais Contribuições
A principal contribuição do artigo é epistêmica, e não matemática, focando na verificação rigorosa de argumentos elementares conhecidos dentro de um assistente de prova formal:

Teorema Principal: Uma prova verificada pelo kernel de que qualquer cobertura de $\mathbb{Z}$ por módulos ímpares distintos $>1$ possui um mmc $> 10.000$ .
Certificados de Capacidade Formalizados: Uma desigualdade aritmética decidível, por cada $N$ , derivada de limites de contagem do CRT que refuta coberturas para $N$ específicos, acompanhada de um lema que garante que esses certificados se aplicam a qualquer subfamília.
Enumeração Verificada pelo Kernel: Uma prova de que a lista de 23 números abundantes ímpares abaixo de 10.000 é completa, utilizando um avaliador especializado projetado para redução de kernel.
Ponte Formal: Uma tradução bidirecional entre a formulação concreta do sistema de cobertura usada na prova e a estrutura StrictCoveringSystem definida no repositório google-deepmind/formal-conjectures. Isso garante que a exclusão se aplique à definição abstrata do problema, e não apenas a exemplos concretos.
Metodologia de Portão de Axiomas (Axiom-Gate): O desenvolvimento limita estritamente sua base de confiança a exatamente três axiomas (propext, Classical.choice, Quot.sound). Exclui explicitamente sorry, native_decide e solvers externos, com verificações de CI automatizadas garantindo que nenhum axioma adicional seja introduzido.

Resultados

A formalização exclui com sucesso todos os números abundantes ímpares $N < 10.000$ como possíveis valores de mmc para um sistema de cobertura ímpar.
A prova estabelece que, se um sistema de cobertura ímpar existir, seu mmc deve ser pelo menos 10.001.
O método mostra ter um limite rígido nos números "rebeldes" (stragglers) 10.395, 12.285 e 17.325, que não são excluídos pelos atuais certificados de capacidade.
O clássico sistema de cobertura de período-12 é verificado para satisfazer todas as hipóteses dos lemas de densidade, enquanto a aritmética de capacidade falha corretamente em excluir este sistema (pois é uma cobertura válida), servindo como um controle de integridade (soundness control).

Significância e Alegações
Os autores declaram explicitamente que este trabalho não resolve o problema de Erdős–Selfridge, nem melhora os limites matemáticos existentes (ex: a classificação de McNew e Setty até $10^6$ ). Em vez disso, a significância reside em:

Certeza Epistêmica: Transformar argumentos de exclusão elementares em teoremas do kernel do Lean, removendo a dependência de literatura não formalizada ou pipelines computacionais não verificados.
Padrão Metodológico: Fornecer um framework reutilizável para "certificados de capacidade" e um padrão para converter exclusões por $N$ em certificados decidíveis processados por decide.
Integração Futura: Estabelecer uma "ponte de periodicidade bidirecional" entre coberturas de $\mathbb{Z}$ e verificações finitas sobre $\mathbb{Z}/N\mathbb{Z}$ . Isso permite que buscas de máquina futuras (como solvers SAT ou enumerações exaustivas) produzam resultados que possam ser consumidos e verificados pelo kernel, em vez de confiar diretamente no output do solver.

O artigo conclui que, embora a exclusão em 10.000 não resolva a questão em aberto, ela fornece uma base verificada e um "encaixe" (socket) portátil para futuras buscas certificadas sobre o problema.

A Descoberta do Artigo: Uma Zona de Exclusão à Prova de Robôs

Por Que Isso Importa (Mesmo Que Não Seja a Resposta Final)

A Conclusão

Mais como este