CINCO CUERPOS, UN NÚMERO FINITO DE DANZAS PERFECTAS

Imagina unas pocas estrellas o planetas dispuestos con tal precisión que todo el grupo puede girar como un objeto rígido, sin cambiar de forma. Para ello, la atracción gravitatoria sobre cada cuerpo debe apuntar exactamente hacia el centro de masas del grupo, con una intensidad proporcional a su distancia a él. Estas disposiciones se llaman configuraciones centrales. Son las formas de las soluciones especiales del problema de los n cuerpos en las que los cuerpos mantienen el mismo patrón relativo, incluidos los equilibrios relativos que giran rígidamente.

Si un patrón funciona, cualquier copia girada, ampliada o desplazada también funciona, así que los matemáticos las cuentan «salvo semejanza».

El sexto problema de Smale

La pregunta es sencilla de enunciar: para cualquier elección de masas positivas, ¿es finito el número de configuraciones centrales? Es el sexto problema de una lista de problemas abiertos elaborada por el matemático Smale.

Así estaban las cosas, según el artículo:

• Tres cuerpos: exactamente cinco, los dos triángulos equiláteros de Lagrange y las tres líneas rectas de Euler.
• Cuatro cuerpos: Hampton y Moeckel demostraron la finitud para todas las masas positivas.
• Cinco cuerpos en un plano: Albouy y Kaloshin demostraron la finitud en 2012, pero solo para masas fuera de un conjunto excepcional, una delgada familia de combinaciones de masas definida por ecuaciones polinómicas, donde su argumento fallaba.

Cerrar el conjunto excepcional

Tejasvi Singh Tomar elimina ese conjunto excepcional. El teorema principal: para toda elección de cinco masas positivas, el problema plano de los cinco cuerpos tiene un número finito de configuraciones centrales salvo semejanza.

La estrategia sigue la de Albouy y Kaloshin. Si hubiera infinitas configuraciones, formarían una curva continua de soluciones al extender las ecuaciones a los números complejos. Siguiendo esa curva «hasta el infinito», las distancias entre los cuerpos deben comportarse de forma que se compensen en un equilibrio preciso. Los cuerpos se acercan a uno de los dieciséis diagramas límite identificados por Albouy y Kaloshin, cada uno de los cuales impone condiciones a las masas.

El nuevo trabajo precisa estas condiciones para toda masa positiva y descarta uno a uno los casos problemáticos:

• las configuraciones en las que cuatro cuerpos forman un cúmulo compacto al que se acerca el quinto se excluyen desarrollando la energía potencial —que se mantiene constante a lo largo de la curva— a órdenes cada vez más altos; para masas positivas, las condiciones resultantes se contradicen;
• se demuestra que otros dos diagramas nunca se producen;
• para todo lo demás, el autor describe todas las condiciones compatibles sobre las masas con álgebra computacional exacta —2.206 sistemas algebraicos— y, para cada uno, produce un certificado numérico: una lista de números racionales cuyas propiedades, comprobadas en aritmética exacta, demuestran que el equilibrio es imposible.

Una trampa tendida por las masas negativas

Hay un obstáculo que el álgebra pura no puede sortear. Otro matemático, Roberts, había encontrado infinitas configuraciones centrales para las masas (1, 1, 1, 1, −¼), con una masa negativa. Cambiando algunos signos, esto se convierte en infinitas soluciones de las ecuaciones complejificadas para las masas (4, 4, 4, 4, 1). No son configuraciones reales, pero un argumento que solo ve las ecuaciones complejas no puede distinguirlas.

Así que, para esas masas, y para la proporción relacionada (1, 1, 4, 4, 4), el autor cuenta directamente las configuraciones reales, con una búsqueda por ordenador que usa aritmética de intervalos garantizada:

• para las masas (1, 4, 4, 4, 4): 306 configuraciones salvo rotación y escala: 60 en línea recta, 24 formando un pentágono convexo y el resto con uno o dos cuerpos en el interior;
• para (1, 1, 4, 4, 4): 294.

Las 60 en línea recta coinciden con un recuento anterior de Moulton.

Verificado por una máquina

Una demostración que descansa en tantos cálculos necesita una verificación sólida. Cada certificado fue comprobado de nuevo por un programa independiente escrito a partir de las definiciones del artículo. Sobre todo, el teorema está demostrado en el asistente de demostración Lean 4, un programa que comprueba cada paso lógico. La demostración formal ni siquiera da por supuestos los resultados de Albouy y Kaloshin: vuelve a deducir lo que necesita y encuentra mediante búsqueda 1.376 diagramas etiquetados que cumplen sus reglas. Otros dos verificadores independientes de demostraciones en Lean la aceptan. Compilarla desde cero lleva unas 860 horas de CPU.

El artículo termina con una breve declaración: se usaron herramientas de IA generativa para encontrar y demostrar los resultados, escribir los programas y la formalización en Lean, y redactar el texto. Las herramientas no se nombran.

Lo que dice y lo que no

El resultado se refiere a cinco cuerpos en un plano. Demuestra que el número de configuraciones es finito para todo conjunto de masas positivas, pero solo da recuentos exactos para las pocas proporciones de masas estudiadas.