🔢 mathematics

A Kernel-Checked Exclusion Certificate for Erd\H{o}s Problem 647

Este artigo apresenta uma prova totalmente verificada e com minimização de axiomas em Lean 4 que resolve o Problema 647 de Erdős para todo $n > 24$ até $10^9$ através do encadeamento de testemunhas de fatoração, com a confiabilidade do resultado reforçada pela reprodução byte a byte em múltiplas ferramentas e arquiteturas independentes.

Autores originais: Ibrahim Mian, Shayaan Siddique

Publicado 2026-08-19

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

Na vasta paisagem da matemática, existem questões que parecem simples na superfície, mas escondem profundas complexidades dentro da estrutura dos números. Uma dessas questões, formulada décadas atrás pelo lendário matemático Paul Erdős, diz respeito à relação entre um número e seus divisores. Todo número inteiro possui um conjunto de números menores que o dividem exatamente; por exemplo, o número seis é divisível por um, dois, três e seis. A contagem desses divisores varia drasticamente de um número para outro. Erdős perguntou-se se existe um padrão específico onde um número é tão "rico" em divisores que força uma certa desigualdade matemática a ser verdadeira para todos os números maiores. Por muito tempo, computadores buscaram por tal número, verificando bilhões e bilhões de candidatos, mas só foram capazes de dizer: "Ainda não encontramos um". Essas buscas, embora poderosas, baseiam-se em métodos computacionais padrão que não oferecem certeza matemática absoluta, deixando uma pequena lacuna de dúvida.

Um novo estudo finalmente fechou essa lacuna para uma enorme faixa de números, não encontrando uma solução, mas provando com absoluta certeza que nenhuma solução existe abaixo de um limite específico. Os pesquisadores, trabalhando com uma equipe de cientistas da computação, usaram um sistema de software especializado projetado para verificar provas matemáticas com o mesmo rigor de um matemático humano checando cada passo de um argumento. Eles focaram no intervalo de números entre vinte e cinco e um bilhão. Usando um método que decompõe o problema em milhões de pequenas partes verificáveis, eles demonstraram que, para cada um dos números nesse vasto intervalo, a condição descrita por Erdős falha. Isso não é um palpite baseado em como os números parecem ou um resultado de uma simulação que possa conter um erro oculto. Em vez disso, toda a cadeia de raciocínio foi checada por um programa de computador que atua como um árbitro imparcial, confirmando que a lógica se sustenta sem atalhos ou suposições não verificadas.

O cerne desta conquista reside em como os pesquisadores lidaram com o volume colossal de dados necessários para cobrir um intervalo tão grande. Eles não tentaram verificar cada número individualmente de uma forma que levaria uma eternidade. Em vez disso, criaram uma cadeia de "testemunhas". Imagine uma série de pedras de toque em um rio; se você puder provar que cada pedra é sólida e que o espaço entre uma pedra e a próxima é pequeno o suficiente para um salto, você pode atravessar o rio inteiro sem cair. Neste caso, as "pedras" são números específicos que provam que a desigualdade falha para todo um bloco de números ao redor. Os pesquisadores geraram mais de seis milhões dessas testemunhas para cobrir o intervalo de vinte e cinco até um bilhão. Cada testemunha é um número que foi cuidadosamente analisado para mostrar que força a quebra da condição matemática. A genialidade do trabalho é que o sistema de verificação computacional não apenas confia na lista de testemunhas; ele recalcula as propriedades de cada uma do zero, confirmando que elas são válidas e que se encaixam perfeitamente para não deixar lacunas na cobertura.

Para garantir que os resultados não fossem apenas o produto de um único programa de computador potencialmente falho, a equipe construiu um sistema de verificações cruzadas que vai muito além da prática científica padrão. Eles escreveram um segundo programa de computador, completamente diferente, escrito em uma linguagem distinta e utilizando um método diferente, para reproduzir toda a cadeia de testemunhas. Este programa independente checou cada passo, confirmando que os números eram válidos e que a lógica se sustentava. Além disso, testaram todo o processo em diferentes tipos de hardware de computador e com diferentes ferramentas de software subjacentes. Eles reconstruíram todo o sistema do zero em máquinas separadas, garantindo que os arquivos digitais finais fossem idênticos até o último bit. Este nível de escrutínio significa que o resultado não depende da confiabilidade de uma máquina específica ou de um código específico, mas da lógica fundamental da própria prova. Os pesquisadores também abordaram uma afirmação anterior que sugeria que uma solução poderia existir, mostrando que a lógica usada naquele esforço anterior continha uma falha crítica que este novo método rigoroso evitou.

A significância deste trabalho estende-se para além de apenas responder a uma questão sobre números. Ela demonstra uma nova forma de fazer matemática onde a confiabilidade de um resultado é construída no próprio processo. No passado, quando computadores eram usados para resolver problemas complexos, os matemáticos frequentemente tinham que confiar que o computador não havia cometido um erro ou que o código estava livre de bugs. Aqui, o computador é usado não apenas para calcular, mas para verificar o cálculo com um nível de certeza que não deixa margem para dúvidas. Os pesquisadores provaram que, para cada número entre vinte e cinco e um bilhão, a condição descrita por Erdős não se mantém. Eles não encontraram um número que satisfaça a condição, nem provaram que tal número não exista em todo o universo dos números. Eles simplesmente provaram que, se tal número existir, ele deve ser maior que um bilhão. Isso deixa a porta aberta para a possibilidade de uma solução no vasto território inexplorado além desse limite, mas fecha firmemente a porta para todo o intervalo que anteriormente era verificado apenas por métodos menos certos.

O estudo também destaca a importância de ser capaz de verificar as ferramentas utilizadas para o trabalho. Os pesquisadores foram cuidadosos para garantir que seu próprio software não dependesse de quaisquer suposições ocultas ou atalhos não comprovados. Eles removeram qualquer parte do processo que não pudesse ser verificada pela lógica central do sistema. Esta abordagem garante que o resultado seja tão sólido quanto os fundamentos matemáticos sobre os quais repousa. Embora a busca por uma solução continue para números maiores que um bilhão, com outros pesquisadores expandindo os limites muito além usando métodos diferentes, este trabalho fornece uma base de certeza para o intervalo que cobre. Ele mostra que, mesmo em um campo tão abstrato quanto a teoria dos números, é possível construir uma ponte de lógica que seja tão forte que possa ser percorrida com total confiança, não deixando dúvidas sobre o caminho tomado. O resultado é uma resposta clara e definitiva para uma questão de longa data para um intervalo específico e massivo de números, alcançada através de uma colaboração de insight humano e precisão de máquina que estabelece um novo padrão para o que é possível na pesquisa matemática.

Resumo Técnico: Um Certificado de Exclusão Verificado pelo Kernel para o Problema de Erdős 647

Enunciado do Problema
O Problema de Erdős 647, proposto por Erdős e Selfridge, questiona se existe um inteiro $n > 24$ tal que $\max_{m<n} (m + \tau(m)) \le n + 2$ , onde $\tau(m)$ é a função de contagem de divisores. Embora a condição seja válida para $n=24$ , e o limite $n+2$ seja estrito, conjectura-se que não existam mais soluções. Buscas computacionais anteriores excluíram soluções até $n \approx 9,17 \times 10^{18}$ usando céus segmentados (segmented sieves) e reduções modulares. No entanto, essas computações dependem de código não verificado, táticas decide nativas ou axiomas específicos do problema, colocando-as fora do kernel de prova confiável de sistemas de verificação formal.

Metodologia e Design do Certificado
Este artigo apresenta uma prova formal em Lean 4 que exclui soluções para $24 < n \le 10^9$ . A prova baseia-se em um formato de certificado de "cadeia de testemunhas" (witness-chain) projetado para ser verificado eficientamente pelo kernel do Lean sem exigir a fatoração completa de cada número.

Definição de Testemunha: Uma "testemunha de morte" (kill witness) $m$ para um alvo $n$ é definida como um inteiro onde $m < n$ e $m + \tau(m) \ge n + 3$ . Tal testemunha refuta a desigualdade para todos os $n$ no intervalo $[m+1, m + \tau(m) - 3]$ .
Otimização da Parte Suave (Smooth Part): Para minimizar a carga de trabalho do kernel, as testemunhas não armazenam fatorações completas de cada número. Em vez disso, elas armazenam a potência máxima de cada primo $p < 1024$ $p < 1024$ que divide $m$ $m$ .
- O kernel verifica que o produto dessas potências de primos armazenadas divide $m$ .
- Ele verifica que cada potência armazenada é máxima (ou seja, $p^{e+1} \nmid m$ ).
- Ele computa um limite inferior para $\tau(m)$ como $\prod (e_i + 1)$ .
- A Regra do Dobro: Se o cofator restante de $m$ (a parte de $m$ não divisível por primos $< 1024$ ) for maior que 1, o limite é dobrado. Isso é válido porque o cofator é coprimo com a parte suave; se ele existir, contribui com pelo menos dois divisores (1 e ele mesmo).
- A primalidade dos primos listados ( $< 1024$ ) é verificada via divisão por tentativa até 31, não exigindo certificados de primalidade externos.
Encadeamento Ganancioso (Greedy Chaining): O certificado é uma sequência de testemunhas geradas de forma gananciosa. Começando da posição de cobertura 24, o algoritmo seleciona uma testemunha $m \le C$ que maximiza a nova posição de cobertura $m + \tau(m) - 3$ . Esta cadeia de 6.685.922 testemunhas cobre todo o intervalo $(24, 10^9]$ .
Estrutura de Formalização: O desenvolvimento em Lean separa uma "camada de sonoridade" (provando a lógica do verificador) da "camada de dados" (as listas de testemunhas). Os dados são codificados como literais em arquivos de origem Lean. O kernel avalia esses literais para verificar a continuidade da cadeia e a validade dos limites.

Contribuições Principais e Verificação
O artigo fornece cinco camadas distintas de verificação e contribuição:

Fechamento de Axiomas: O teorema final é provado com um fechamento de axiomas de exatamente $\{ \text{propext}, \text{Classical.choice}, \text{Quot.sound} \}$ . Ele não contém sorry, nenhum native decide ou axiomas específicos do problema.
Replay Independente: O script gerador é explicitamente não confiável. Uma segunda implementação em Python, independente (usando divisão por tentativa), reproduz cada testemunha para verificar a primalidade, a ordenação e a condição do dobro. Uma terceira implementação computa independentemente a função de divisores e confirma que o conjunto de soluções coincide com a OEIS A087280.
Reprodutibilidade a partir da Fonte: Duas pernas de verificação independentes em hardware x86 separado compilaram a ferramenta Lean a partir da fonte (usando gcc e clang), reconstruíram o mathlib e o desenvolvimento sem cache, e regeneraram os arquivos de certificado. Os arquivos .olean resultantes foram byte a byte idênticos ao build original em ARM, com dígitos SHA-256 idênticos.
Verificação Autônoma (Standalone): O desenvolvimento compilado foi re-tipado usando o lean4checker autônomo, contornando o elaborador, confirmando a integridade dos artefatos compilados.
Correção de um Design Falho: O artigo documenta uma iteração de design onde um gerador estagnava em um "mínimo de lacuna" (gap minimum) porque falhava em considerar a regra do dobro quando um grande primo ( $>1024$ ) reduzia o número de divisores pela metade. A inclusão da regra de maximalidade-e-dobro resolveu isso, demonstrando o valor de uma geração que "falha ruidosamente" (fail-loud) para o fortalecimento da sonoridade.

Resultados
O resultado principal é o Teorema 1.1: Nenhum inteiro $n$ com $24 < n \le 10^9$ satisfaz $\max_{m<n} (m + \tau(m)) \le n + 2$ .

A prova cobre o intervalo $(24, 10^9]$ usando uma cadeia de 6.685.922 testemunhas.
O certificado para $10^9$ é de aproximadamente 260 MB de código-fonte, enviado como um artefato de release versionado.
Os intervalos de $10^7$ e $10^8$ são impostos em integração contínua; o intervalo de $10^9$ foi verificado pelo kernel uma vez sob a ferramenta clang e verificado via pipeline de replay independente.

Significância e Escopo
O artigo afirma explicitamente que não encerra o Problema de Erdős 647, nem pretende alcançar as fronteiras computacionais de outros pesquisadores (Idén, Hughes, bentrd), que se estendem até $10^{18}$ .

Confiança vs. Alcance: A contribuição é a base de confiança, não o alcance. O trabalho desloca a verificação da não existência no intervalo $(24, 10^9]$ de uma computação não verificada para uma prova verificada pelo kernel.
Finito vs. Assintótico: O trabalho aborda uma lacuna específica de uma alegação retirada de janeiro de 2026. Essa alegação tentava provar o problema via "intervalos de dominação" cobrindo todos os $n > 24$ , mas falhou em provar que os intervalos se sobrepõem assintoticamente. Este artigo demonstra que a forma finita desse argumento (cobrindo um intervalo limitado) é um fato verificável que um kernel de prova pode estabelecer.
Limites Futuros: Os autores observam que o método é limitado pelo tamanho do certificado e pelo tempo do kernel, não pela matemática. Estender o alcance para $10^{10}$ exigiria ~2 GB de código-fonte, e $10^{12}$ seria inviável com esta representação. Trabalhos futuros exigiriam a certificação de reduções modulares (argumentos estruturais) em vez de cadeias lineares de testemunhas.

Em resumo, o artigo estabelece um novo padrão para busca certificada: uma exclusão finita, totalmente provada, de soluções até $10^9$ que depende exclusivamente do kernel do Lean e de axiomas padrão, sendo independente da confiabilidade do gerador.

Mais como este