Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proof

Resumo Técnico: Resolução do Problema de Erdős #728

Enunciado do Problema
O artigo aborda o Problema de Erdős #728, que investiga o tamanho máximo possível da lacuna $k := a + b - n$ sob a restrição de divisibilidade fatorial:
$$a! b! \mid n! (a + b - n)!$$
Sem restrições adicionais, existem soluções triviais onde $k$ pode ser arbitrariamente grande (por exemplo, ao tomar $a$ e $b$ muito grandes). Para tornar o problema não trivial, os autores impõem a condição de que $a$ e $b$ estejam afastados dos extremos, especificamente $\varepsilon n \le a, b \le (1-\varepsilon)n$ para algum $0 < \varepsilon < 1/2$. O objetivo é determinar quão grande $k$ pode ser em relação a $n$ sob essas restrições.

Metodologia e Estratégia de Prova
A prova procede transformando a condição de divisibilidade fatorial em um problema de coeficientes binomiais e valuações $p$-ádicas.

1. Redução à Divisibilidade Binomial:
   Ao definir $n = 2m$, $b = m$ e $a = m + k$, a condição original é equivalente a:
   $$\binom{m+k}{k} \mid \binom{2m}{m}$$
   Isso requer mostrar que, para cada primo $p$, a valuação $p$-ádica do lado esquerdo é menor ou igual à do lado direito:
   $$\nu_p\left(\binom{m+k}{k}\right) \le \nu_p\left(\binom{2m}{m}\right)$$

2. Análise de Valuação via Teorema de Kummer:
   Usando o teorema de Kummer, $\nu_p\left(\binom{2m}{m}\right)$ é identificado com o número de transportes (carries) que ocorrem ao somar $m + m$ na base $p$. O termo $\nu_p\left(\binom{m+k}{k}\right)$ é limitado pela valuação máxima de qualquer termo no bloco consecutivo $m+1, \dots, m+k$, denotada por $V_p(m, k)$.
   A desigualdade central a ser satisfeita é:
   $$V_p(m, k) \le \kappa_p(m)$$
   onde $\kappa_p(m)$ é a contagem de transportes para $m+m$ na base $p$.

3. Análise Primo a Primo:
   Os autores dividem a análise em dois regimes baseados no tamanho do primo $p$ em relação a $k$:

   • Primos Grandes ($p > 2k$): Neste intervalo, a desigualdade é satisfeita automaticamente. Como o comprimento do intervalo $k$ é menor que $p/2$, no máximo um número no bloco $m+1, \dots, m+k$ pode ser divisível por $p$. Se uma potência alta $p^J$ divide um termo, os dígitos na base $p$ de $m$ forçam pelo menos $J$ transportes quando duplicados, satisfazendo a condição.
   • Primos Pequenos ($p \le 2k$): Esta é a principal dificuldade. Os autores empregam um argumento de contagem probabilística para encontrar um inteiro $m$ em um grande intervalo $[M, 2M]$ que satisfaça simultaneamente duas condições para todos os $p \le 2k$:
     • Rico em Transportes (Carry-Rich): A expansão na base $p$ de $m$ possui muitos dígitos $\ge \lceil p/2 \rceil$ nas primeiras $L_p$ posições. Isso força um alto número de transportes ($\kappa_p(m)$) quando $m$ é duplicado.
     • Livre de Picos (Spike-Free): Nenhum inteiro no bloco $m+1, \dots, m+k$ é divisível por uma potência de $p$ incomumente alta (especificamente, $V_p(m, k)$ é mantido abaixo de um limite $J_p + t(M)$).

4. Existência via Limite Superior da União (Union Bound):
   Os autores definem conjuntos "ruins" de inteiros $m$ que falham tanto na condição de transporte quanto na condição de pico. Usando limites de Chernoff para a distribuição de dígitos grandes e contagem simples para a condição de pico, eles mostram que a medida total desses conjuntos ruins é estritamente menor que o tamanho do intervalo $[M, 2M]$. Consequentemente, um $m$ "bom" existe que satisfaz a condição de divisibilidade para todos os primos relevantes simultaneamente.

Resultados Principais
O artigo estabelece o Teorema 1 (Janela de lacuna logarítmica):
Para quaisquer constantes $0 < C_1 < C_2$ e $0 < \varepsilon < 1/2$, existem infinitas triplas $(a, b, n) \in \mathbb{N}^3$ tais que:

1. $\varepsilon n \le a, b \le (1-\varepsilon)n$
2. $a! b! \mid n! (a + b - n)!$
3. $C_1 \log n < a + b - n < C_2 \log n$

A construção produz uma lacuna $k$ que cresce logaritmicamente com $n$. Os autores observam que a prova atual produz $k \asymp \log n$, mas o método poderia potencialmente ser estendido para $k = \exp(c\sqrt{\log n})$ com refinamentos adicionais, embora o texto atual foque no regime logarítmico.

Significância e Alegações

• Primeiro Problema de Erdős Resolvido por IA: Os autores afirmam que este é o primeiro problema de Erdős a ser "totalmente resolvido de forma autônoma por um sistema de IA". O sistema utilizado foi uma combinação do GPT-5.2 Pro e o provador de teoremas "Aristotle" da Harmonic.
• Verificação Formal: A prova foi gerada como uma prova formal no provador de teoremas Lean e, posteriormente, traduzida para a matemática informal apresentada neste resumo.
• Contribuição Metodológica: O trabalho estende técnicas anteriores de Erdős e Pomerance sobre divisores de coeficientes binomiais centrais. Diferente de trabalhos anteriores que focavam em inteiros "pobres em transportes" (poucos transportes) ou tamanhos de lacuna fixos, esta prova constrói inteiros "ricos em transportes" para lidar com uma janela crescente de tamanho $k \asymp \log n$.
• Independência: Os autores observam que, após o trabalho inicial deles, Carl Pomerance derivou independentemente resultados semelhantes, e modificações deste argumento foram usadas para resolver os Problemas de Erdős #729 e #401.

O artigo não afirma resolver o problema em sua forma absolutamente mais forte (notando o potencial para lacunas maiores), mas assegura a resolução bem-sucedida da questão específica da lacuna logarítmica proposta por Erdős.