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

Resumen Técnico: Resolución del Problema de Erdős #728

Enunciado del Problema
El artículo aborda el Problema de Erdős #728, el cual investiga el tamaño máximo posible de la brecha $k := a + b - n$ bajo la restricción de divisibilidad factorial:
$$a! b! \mid n! (a + b - n)!$$
Sin restricciones adicionales, existen soluciones triviales donde $k$ es arbitrariamente grande (por ejemplo, tomando $a$ y $b$ muy grandes). Para que el problema sea no trivial, los autores imponen la condición de que $a$ y $b$ estén alejados de los extremos, específicamente $\varepsilon n \le a, b \le (1-\varepsilon)n$ para algún $0 < \varepsilon < 1/2$. El objetivo es determinar qué tan grande puede ser $k$ en relación con $n$ bajo estas restricciones.

Metodología y Estrategia de Demostración
La demostración procede transformando la condición de divisibilidad factorial en un problema relativo a coeficientes binomiales y valuaciones $p$-ádicas.

1. Reducción a la Divisibilidad Binomial:
   Al establecer $n = 2m$, $b = m$, y $a = m + k$, la condición original es equivalente a:
   $$\binom{m+k}{k} \mid \binom{2m}{m}$$
   Esto requiere demostrar que para cada primo $p$, la valuación $p$-ádica del lado izquierdo es menor o igual que la del lado derecho:
   $$\nu_p\left(\binom{m+k}{k}\right) \le \nu_p\left(\binom{2m}{m}\right)$$

2. Análisis de Valuación mediante el Teorema de Kummer:
   Utilizando el teorema de Kummer, $\nu_p\left(\binom{2m}{m}\right)$ se identifica con el número de acarreos que ocurren al sumar $m + m$ en base $p$. El término $\nu_p\left(\binom{m+k}{k}\right)$ está acotado por la valuación máxima de cualquier término en el bloque consecutivo $m+1, \dots, m+k$, denotada como $V_p(m, k)$. La desigualdad central a satisfacer es:
   $$V_p(m, k) \le \kappa_p(m)$$
   donde $\kappa_p(m)$ es el conteo de acarreos para $m+m$ en base $p$.

3. Análisis Primo por Primo:
   Los autores dividen el análisis en dos regímenes basados en el tamaño del primo $p$ relativo a $k$:

   • Primos Grandes ($p > 2k$): En este rango, la desigualdad se cumple automáticamente. Dado que la longitud del intervalo $k$ es menor que $p/2$, a lo sumo un número en el bloque $m+1, \dots, m+k$ puede ser divisible por $p$. Si una potencia alta $p^J$ divide a un término, los dígitos en base $p$ de $m$ fuerzan al menos $J$ acarreos al duplicarse, satisfaciendo la condición.
   • Primos Pequeños ($p \le 2k$): Esta es la dificultad principal. Los autores emplean un argumento de conteo probabilístico para encontrar un entero $m$ en un intervalo grande $[M, 2M]$ que satisfaga simultáneamente dos condiciones para todo $p \le 2k$:
     • Rico en Acarreos (Carry-Rich): La expansión en base $p$ de $m$ tiene muchos dígitos $\ge \lceil p/2 \rceil$ en las primeras $L_p$ posiciones. Esto fuerza un alto número de acarreos ($\kappa_p(m)$) cuando $m$ es duplicado.
     • Libre de Picos (Spike-Free): Ningún entero en el bloque $m+1, \dots, m+k$ es divisible por una potencia inusualmente alta de $p$ (específicamente, $V_p(m, k)$ se mantiene por debajo de un umbral $J_p + t(M)$).

4. Existencia mediante la Cota de Unión (Union Bound):
   Los autores definen conjuntos "malos" de enteros $m$ que fallan tanto en la condición de acarreos como en la condición de picos. Utilizando las cotas de Chernoff para la distribución de dígitos grandes y el conteo simple para la condición de picos, demuestran que la medida total de estos conjuntos malos es estrictamente menor que el tamaño del intervalo $[M, 2M]$. Por consiguiente, existe un $m$ "bueno" que satisface la condición de divisibilidad para todos los primos relevantes simultáneamente.

Resultados Clave
El artículo establece el Teorema 1 (Ventana de brecha logarítmica):
Para cualesquiera constantes $0 < C_1 < C_2$ y $0 < \varepsilon < 1/2$, existen infinitas ternas $(a, b, n) \in \mathbb{N}^3$ tales 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$

La construcción produce una brecha $k$ que crece logarítmicamente con $n$. Los autores señalan que la demostración actual arroja $k \asymp \log n$, pero el método podría extenderse potencialmente a $k = \exp(c\sqrt{\log n})$ con un mayor refinamiento, aunque el escrito actual se centra en el régimen logarítmico.

Significancia y Reivindicaciones

• Primer Problema de Erdős Resuelto por IA: Los autores afirman que este es el primer problema de Erdős que ha sido "resuelto completamente de forma autónoma por un sistema de IA". El sistema utilizado fue una combinación de GPT-5.2 Pro y el probador de teoremas "Aristotle" de Harmonic.
• Verificación Formal: La demostración fue generada como una prueba formal en el probador de teoremas Lean y posteriormente traducida a la matemática informal presentada en este resumen.
• Contribución Metodológica: El trabajo extiende técnicas previas de Erdős y Pomerance respecto a los divisores de coeficientes binomiales centrales. A diferencia de trabajos previos que se centraban en enteros "pobres en acarreos" (pocos acarreos) o tamaños de brecha fijos, esta demostración construye enteros "ricos en acarreos" para manejar una ventana creciente de tamaño $k \asymp \log n$.
• Independencia: Los autores señalan que, tras su trabajo inicial, Carl Pomerance derivó de forma independiente resultados similares, y que modificaciones de este argumento fueron utilizadas para resolver los Problemas de Erdős #729 y #401.

El artículo no pretende resolver el problema en su forma más fuerte posible (notando el potencial para brechas mayores), sino que afirma la resolución exitosa de la pregunta específica de la brecha logarítmica planteada por Erdős.