The lonely runner conjecture holds for nine runners

Resumen Técnico: La Conjetura del Corredor Solitario para Nueve Corredores

Planteamiento del Problema
El artículo aborda la Conjetura del Corredor Solitario, un problema abierto de larga data en la teoría de números combinatoria, propuesto por primera vez por Wills en 1967. La conjetura postula que para cualquier entero $k \ge 1$ y cualquier conjunto de $k$ enteros distintos (que representan las velocidades de los corredores) $v_1, \dots, v_k$, existe un tiempo real $t$ tal que cada corredor es "solitario". Matemáticamente, esto significa que existe un $t$ donde la distancia de cada corredor al origen en un círculo unitario es al menos $1/(k+1)$, expresado como $\|t v_i\| \ge 1/(k+1)$ para todo $i$.

Si bien la conjetura ha sido verificada para valores pequeños de $k$ (hasta $k=7$), sigue abierta en el caso general. Este artículo se dirige específicamente al caso de nueve corredores ($k=9$).

Metodología
La estrategia de prueba se basa en el trabajo previo de los autores que estableció la conjetura para ocho corredores. El argumento central se basa en una prueba por contradicción que involucra las propiedades de un hipotético "contraejemplo mínimo".

1. Reducción a Restricciones de Divisibilidad:
   La prueba utiliza un límite derivado por Malikiosis, Santos y Schymura (Teorema 1), que implica que si la conjetura se cumple para $k$, se cumple para $k+1$ siempre que el producto de las velocidades en cualquier contraejemplo mínimo supere un umbral específico. En consecuencia, para probar la conjetura para $k+1$, basta con demostrar que no existe un conjunto de $k$ velocidades que viole la "propiedad del corredor solitario" (propiedad LR) mientras satisface las restricciones de divisibilidad impuestas por el límite.

2. Lema Generalizado para Divisores:
   Los autores introducen el Lema 6, una versión fortalecida y generalizada de un lema anterior (Lema 3). Este lema establece las condiciones bajo las cuales un entero $d$ específico debe dividir el producto de las velocidades de cualquier conjunto de 8 enteros que carece de la propiedad LR.

   • El lema introduce un coeficiente $c$ y considera las velocidades módulo $9cd$.
   • Incorpora condiciones de divisibilidad específicas respecto al número de velocidades divisibles por 3 y 9 (derivadas del Lema 5).
   • La condición requiere verificar que para cualquier conjunto de 8 velocidades que satisfaga ciertas restricciones de MCD y divisibilidad, exista un tiempo $t$ que satisfaga la propiedad LR.

3. Verificación Asistida por Computadora (Reformulación de Cobertura de Conjuntos):
   Verificar las condiciones del Lema 6 es computacionalmente intensivo. Los autores reformulan el problema como un problema de cobertura de conjuntos (Lema 7).

   • Un entero $v$ "cubre" un entero $j$ si $\| \frac{jv}{9cd} \| < 1/8$.
   • El objetivo es verificar que no exista un 8-tupla "mala" que cubra todos los enteros necesarios mientras satisface las restricciones de divisibilidad.
   • Los autores implementaron un algoritmo de retroceso (backtracking) con optimizaciones significativas sobre su trabajo previo para $k=7$:
     • Precomputación de bitsets para las posiciones cubiertas.
     • Estrategias de poda basadas en el número máximo de nuevos enteros que un elemento candidato puede cubrir.
     • Memoización para eliminar rutas de búsqueda redundantes.
   • Los autores también probaron enfoques de solucionadores SAT (usando Cardinality-CDCL y Minicard), pero encontraron que eran significativamente más lentos que su implementación personalizada de backtracking para esta estructura de problema específica.

Contribuciones Clave y Resultados

• Prueba para Nueve Corredores: El artículo proporciona una prueba completa de que la Conjetura del Corredor Solitario se cumple para $k=9$.
• Identificación de Divisores: Al aplicar el Lema 6 con un programa computacional, los autores identificaron un conjunto $S$ de enteros (que incluye potencias de primos como $64, 81, 25$ y primos hasta 191) que deben dividir el producto de las velocidades en cualquier contraejemplo mínimo para 9 corredores.
• Contradicción: El producto de los elementos en el conjunto $S$ (que son coprimos entre sí) es aproximadamente $9.09 \times 10^{79}$. Sin embargo, el límite superior teórico para el producto de las velocidades en un contraejemplo mínimo (derivado de la Corolario 2) es aproximadamente $8.47 \times 10^{79}$. Dado que el producto requerido de los divisores excede el producto máximo posible de las velocidades, no puede existir tal contraejemplo.
• Mejoras Algorítmicas: El artículo detalla las mejoras de implementación que redujeron el tiempo de ejecución para el caso de verificación de $k=7$ de 32 horas a 50 minutos, permitiendo la verificación más compleja de $k=9$.

Significado y Reivindicaciones
Los autores afirman que este resultado extiende el rango conocido de la Conjetura del Corredor Solitario de 7 a 9 corredores. Observan que la técnica utilizada es teóricamente aplicable a cualquier número específico de corredores, aunque el costo computacional crece rápidamente.

• Independencia: Los autores reconocen que Trakulthongchai anunció independientemente pruebas para $k=9$ y $k=10$ poco antes de esta entrega. El trabajo de Trakulthongchai también se basa en la prueba de $k=7$ y utiliza un "método de cribado ingenioso" que parece ser aproximadamente 100 veces más rápido que el método presentado aquí.
• Perspectiva Futura: El artículo discute la viabilidad de extender esto a $k=10$. Aunque el método es adaptable, se estima que el costo computacional para verificar primos hasta aproximadamente 263 tomaría dos años en un solo núcleo. Los autores sugieren que combinar sus mejoras (como considerar potencias de primos pequeños) con el enfoque de cribado de Trakulthongchai podría hacer que el caso de $k=10$ sea más tratable, pero no pretenden haberlo resuelto ellos mismos.

En resumen, el artículo resuelve con éxito el caso de $k=9$ mediante una combinación de lemas teóricos refinados y una verificación computacional altamente optimizada, posicionando modestamente el trabajo como un paso adelante que se beneficia y contribuye al esfuerzo más amplio por resolver la conjetura para un mayor número de $k$.