🔢 mathematics

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

Este artículo presenta una prueba totalmente verificada y de axiomas minimizados en Lean 4 que resuelve el Problema 647 de Erdős para todo $n > 24$ hasta $10^9$ mediante la encadenación de testigos de factorización, con la confiabilidad del resultado reforzada por la reproducción de bytes idénticos a través de múltiples cadenas de herramientas y arquitecturas independientes.

Autores originales: Ibrahim Mian, Shayaan Siddique

Publicado 2026-08-19

📖 6 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Ibrahim Mian, Shayaan Siddique

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

En el vasto paisaje de las matemáticas, existen preguntas que parecen simples en la superficie pero que esconden profundas complejidades dentro de la estructura de los números. Una de estas preguntas, planteada hace décadas por el legendario matemático Paul Erdős, se refiere a la relación entre un número y sus divisores. Todo número entero tiene un conjunto de números más pequeños que lo dividen exactamente; por ejemplo, el número seis es divisible por uno, dos, tres y seis. El recuento de estos divisores varía enormemente de un número a otro. Erdős se preguntó si existe un patrón específico donde un número sea tan "rico" en divisores que obligue a que se cumpla una cierta desigualdad matemática para todos los números mayores. Durante mucho tiempo, las computadoras han buscado tal número, examinando miles de millones de candidatos, pero solo han podido decir: "Aún no hemos encontrado uno". Estas búsquedas, aunque potentes, dependen de métodos informáticos estándar que no ofrecen una certeza matemática absoluta, dejando un pequeño margen de duda.

Un nuevo estudio finalmente ha cerrado ese vacío para un rango masivo de números, no encontrando una solución, sino demostrando con absoluta certeza que no existe ninguna solución por debajo de un umbral específico. Los investigadores, trabajando con un equipo de científicos de la computación, utilizaron un sistema de software especializado diseñado para verificar pruebas matemáticas con el mismo rigor que un matemático humano revisando cada uno de los pasos de un argumento. Se centraron en el rango de números entre veinticinco y mil millones. Utilizando un método que descompone el problema en millones de piezas diminutas y verificables, demostraron que para cada uno de los números en este vasto intervalo, la condición descrita por Erdős falla. Esto no es una suposición basada en cómo se ven los números o un resultado de una simulación que pueda contener un error oculto. En cambio, toda la cadena de razonamiento ha sido revisada por un programa informático que actúa como un árbitro imparcial, confirmando que la lógica se mantiene sin atajos ni supuestos no verificados.

El núcleo de este logro reside en cómo los investigadores manejaron el enorme volumen de datos necesarios para cubrir un rango tan grande. No intentaron comprobar cada número individualmente de una manera que tomara una eternidad. En su lugar, crearon una cadena de "testigos". Imagine una serie de piedras de paso a través de un río; si puede demostrar que cada piedra es sólida y que el espacio entre una piedra y la siguiente es lo suficientemente pequeño como para saltar, puede cruzar todo el río sin caerse. En este caso, las "piedras" son números específicos que demuestran que la desigualdad falla para todo un bloque de números circundantes. Los investigadores generaron más de seis millones de estos testigos para cubrir todo el intervalo desde veinticinco hasta mil millones. Cada testigo es un número que ha sido analizado cuidadosamente para mostrar que obliga a que la condición matemática se rompa. La brillantez del trabajo es que el sistema de verificación informática no solo confía en la lista de testigos; sino que recalcula las propiedades de cada uno desde cero, confirmando que son válidos y que encajan perfectamente para no dejar huecos en la cobertura.

Para asegurar que los resultados no fueran producto de un único programa informático potencialmente defectuoso, el equipo construyó un sistema de comprobaciones cruzadas que va mucho más allá de la práctica científica estándar. Escribieron un segundo programa informático, completamente diferente, escrito en un lenguaje distinto y utilizando un método diferente, para reproducir toda la cadena de testigos. Este programa independiente comprobó cada uno de los pasos, confirmando que los números eran válidos y que la lógica se mantenía. Además, probaron todo el proceso en diferentes tipos de hardware informático y con diferentes herramientas de software subyacentes. Reconstruyeron todo el sistema desde cero en máquinas separadas, asegurándose de que los archivos digitales finales fueran idénticos hasta el último bit. Este nivel de escrutinio significa que el resultado no depende de la confiabilidad de una máquina específica o de un código específico, sino de la lógica fundamental de la prueba misma. Los investigadores también abordaron una afirmación previa que sugería que podría existir una solución, demostrando que la lógica utilizada en aquel intento anterior tenía un fallo crítico que este nuevo y riguroso método evitó.

La importancia de este trabajo se extiende más allá de simplemente responder una pregunta sobre números. Demuestra una nueva forma de hacer matemáticas donde la confiabilidad de un resultado está integrada en el proceso mismo. En el pasado, cuando se usaban computadoras para resolver problemas complejos, los matemáticos a menudo tenían que confiar en que la computadora no había cometido un error o que el código estaba libre de errores. Aquí, la computadora se utiliza no solo para calcular, sino para verificar el cálculo con un nivel de certeza que no deja lugar a la duda. Los investigadores demostraron que para cada número entre veinticinco y mil millones, la condición descrita por Erdős no se cumple. No encontraron un número que satisfaga la condición, ni demostraron que no exista tal número en absoluto en el universo de los números. Simplemente demostraron que, si tal número existe, debe ser mayor que mil millones. Esto deja la puerta abierta a la posibilidad de una solución en el vasto territorio inexplorado más allá, pero cierra firmemente la puerta en todo el rango que anteriormente solo había sido verificado por métodos menos seguros.

El estudio también destaca la importancia de ser capaz de verificar las herramientas utilizadas para realizar el trabajo. Los investigadores se aseguraron de que su propio software no dependiera de ninguna suposición oculta o atajos no probados. Eliminaron cualquier parte del proceso que no pudiera ser verificada por la lógica central del sistema. Este enfoque asegura que el resultado sea tan sólido como los fundamentos matemáticos sobre los que descansa. Si bien la búsqueda de una solución continúa para números mayores que mil millones, con otros investigadores ampliando los límites mucho más allá utilizando métodos diferentes, este trabajo proporciona una base de certeza para el rango que cubre. Muestra que, incluso en un campo tan abstracto como la teoría de números, es posible construir un puente de lógica que sea tan fuerte que se pueda cruzar con total confianza, sin dejar lugar a dudas sobre el camino recorrido. El resultado es una respuesta clara y definitiva a una pregunta de larga data para un rango específico y masivo de números, lograda mediante una colaboración de la visión humana y la precisión de la máquina que establece un nuevo estándar para lo que es posible en la investigación matemática.

Resumen Técnico: Un Certificado de Exclusión Verificado por el Kernel para el Problema de Erdős 647

Planteamiento del Problema
El Problema de Erdős 647, planteado por Erdős y Selfridge, pregunta si existe un entero $n > 24$ tal que $\max_{m<n} (m + \tau(m)) \le n + 2$ , donde $\tau(m)$ es la función de conteo de divisores. Si bien la condición se cumple para $n=24$ , y el límite $n+2$ es ajustado, se conjetura que no existen más soluciones. Búsquedas computacionales previas han excluido soluciones hasta $n \approx 9.17 \times 10^{18}$ utilizando cribas segmentadas y reducciones modulares. Sin embargo, estos cálculos dependen de código no verificado, tácticas decide nativas o axiomas específicos del problema, lo que los sitúa fuera del kernel de prueba confiable de los sistemas de verificación formal.

Metodología y Diseño del Certificado
Este artículo presenta una prueba formal en Lean 4 que excluye soluciones para $24 < n \le 10^9$ . La prueba se basa en un formato de certificado de "cadena de testigos" diseñado para ser verificado eficientemente por el kernel de Lean sin requerir la factorización completa de cada número.

Definición de Testigo: Un "testigo de muerte" (kill witness) $m$ para un objetivo $n$ se define como un entero donde $m < n$ y $m + \tau(m) \ge n + 3$ . Tal testigo refuta la desigualdad para todo $n$ en el intervalo $[m+1, m + \tau(m) - 3]$ .
Optimización de la Parte Suave (Smooth Part): Para minimizar la carga de trabajo del kernel, los testigos no almacenan factorizaciones completas. En su lugar, almacenan la potencia máxima de cada primo $p < 1024$ $p < 1024$ que divide a $m$ $m$ .
- El kernel verifica que el producto de estas potencias de primos divide a $m$ .
- Verifica que cada potencia almacenada es máxima (es decir, $p^{e+1} \nmid m$ ).
- Computa un límite inferior para $\tau(m)$ como $\prod (e_i + 1)$ .
- La Regla de Duplicación: Si el cofactor restante de $m$ (la parte no divisible por primos $< 1024$ ) es mayor que 1, el límite se duplica. Esto es válido porque el cofactor es coprimo con la parte suave; si existe, contribuye al menos con dos divisores (1 y sí mismo).
- La primalidad de los primos listados ( $< 1024$ ) se verifica mediante división por tentativa por primos hasta 31, lo que no requiere certificados de primalidad externos.
Encadenamiento Voraz (Greedy Chaining): El certificado es una secuencia de testigos generados de forma voraz. Comenzando desde la posición de cobertura 24, el algoritmo selecciona un testigo $m \le C$ que maximiza la nueva posición de cobertura $m + \tau(m) - 3$ . Esta cadena de 6,685,922 testigos cubre todo el intervalo $(24, 10^9]$ .
Estructura de Formalización: El desarrollo en Lean separa una capa de "sonidez" (que prueba la lógica del verificador) de la "capa de datos" (las listas de testigos). Los datos se codifican como literales en archivos fuente de Lean. El kernel evalúa estos literales para verificar la continuidad de la cadena y la validez de los límites.

Contribuciones Clave y Verificación
El artículo proporciona cinco capas distintas de verificación y contribución:

Cierre de Axiomas: El teorema final se demuestra con un cierre de axiomas de exactamente $\{ \text{propext}, \text{Classical.choice}, \text{Quot.sound} \}$ . No contiene ningún sorry, ningún native decide, ni axiomas específicos del problema.
Replay Independiente: El script generador es explícitamente no confiable. Una segunda implementación independiente en Python (usando división por tentativa) reproduce cada testigo para verificar la primalidad, el orden y la condición de duplicación. Una tercera implementación recomputa independientemente la función de divisor y confirma que el conjunto de soluciones coincide con OEIS A087280.
Reproducibilidad desde la Fuente: Dos ejecuciones de verificación independientes en hardware x86 separado compilaron la cadena de herramientas de Lean desde la fuente (usando gcc y clang), reconstruyeron mathlib y el desarrollo sin caché, y regeneraron los archivos de certificado. Los archivos .olean resultantes son byte a byte idénticos al build original de ARM, con identificadores SHA-256 idénticos.
Verificación Independiente (Standalone): El desarrollo compilado fue re-verificado mediante el tipado de tipos independiente lean4checker, confirmando la integridad de los artefactos compilados.
Corrección de un Diseño Defectuoso: El artículo documenta una iteración de diseño donde un generador se estancaba en un "mínimo de brecha" porque no tenía en cuenta la regla de duplicación cuando un primo grande ( $>1024$ ) reducía a la mitad la cuenta de divisores. La inclusión de la regla de maximalidad y duplicación resolvió esto, demostrando el valor de la generación de "falla ruidosa" (fail-loud) en el fortalecimiento de la preservación de la sonidez.

Resultados
El resultado principal es el Teorema 1.1: No existe un entero $n$ con $24 < n \le 10^9$ que satisfaga $\max_{m<n} (m + \tau(m)) \le n + 2$ .

La prueba cubre el rango $(24, 10^9]$ usando una cadena de 6,685,922 testigos.
El certificado para $10^9$ es de aproximadamente 260 MB de código fuente, entregado como un artefacto de lanzamiento versionado.
Los rangos de $10^7$ y $10^8$ se imponen en la integración continua; el rango de $10^9$ fue verificado por el kernel una vez bajo la cadena de herramientas clang y verificado mediante el pipeline de reproducción independiente.

Significado y Alcance
El artículo establece explícitamente que no cierra el Problema de Erdős 647, ni pretende alcanzar las fronteras computacionales de otros investigadores (Idén, Hughes, bentrd), que se extienden hasta $10^{18}$ .

Confianza vs. Rango: La contribución es la base de confianza, no el rango. El resultado traslada la verificación de la no existencia en el rango $(24, 10^9]$ de una computación no verificada a una prueba verificada por el kernel.
Finito vs. Asintótico: El trabajo aborda un vacío específico en una afirmación retirada de enero de 2026. Dicha afirmación intentaba probar el problema mediante "intervalos de dominación" que cubrían todos los $n > 24$ , pero falló al intentar probar que los intervalos se solapan asintóticamente. Este artículo demuestra que la forma finita de ese argumento (cubrir un rango acotado) es un hecho verificable que un kernel de prueba puede establecer.
Límites Futuros: Los autores señalan que el método está limitado por el tamaño del certificado y el tiempo del kernel, no por las matemáticas. Extender el rango a $10^{10}$ requeriría ~2 GB de código fuente, y $10^{12}$ sería inviable con esta representación. El trabajo futuro requeriría certificar reducciones modulares (argumentos estructurales) en lugar de cadenas de testigos lineales.

En resumen, el artículo establece un nuevo estándar para la búsqueda certificada: una exclusión finita y totalmente probada de soluciones hasta $10^9$ que depende únicamente del kernel de Lean y de los axiomas estándar, independientemente de la confiabilidad del generador.

Más como este