CINCO CORPOS, UM NÚMERO FINITO DE DANÇAS PERFEITAS
Imagine algumas estrelas ou planetas dispostos com tanta precisão que o grupo inteiro pode girar como um objeto rígido, sem mudar de forma. Para isso, a atração gravitacional sobre cada corpo precisa apontar exatamente para o centro de massa do grupo, com uma intensidade proporcional à sua distância até ele. Esses arranjos são chamados de configurações centrais. São as formas das soluções especiais do problema de n corpos em que os corpos mantêm o mesmo padrão relativo, incluindo os equilíbrios relativos que giram rigidamente.
Se um padrão funciona, qualquer cópia dele girada, ampliada ou deslocada também funciona; por isso os matemáticos as contam “a menos de semelhança”.
O sexto problema de Smale
A pergunta é simples de enunciar: para qualquer escolha de massas positivas, o número de configurações centrais é finito? É o sexto problema de uma lista de problemas em aberto elaborada pelo matemático Smale.
Eis a situação, segundo o artigo:
- Três corpos: exatamente cinco — os dois triângulos equiláteros de Lagrange e as três linhas retas de Euler.
- Quatro corpos: a finitude foi provada por Hampton e Moeckel, para todas as massas positivas.
- Cinco corpos num plano: Albouy e Kaloshin provaram a finitude em 2012, mas apenas para massas fora de um conjunto excepcional — uma família estreita de combinações de massas definida por equações polinomiais, onde o argumento deles falhava.
Fechando o conjunto excepcional
Tejasvi Singh Tomar elimina esse conjunto excepcional. O teorema principal: para qualquer escolha de cinco massas positivas, o problema planar de cinco corpos tem um número finito de configurações centrais a menos de semelhança.
A estratégia segue a de Albouy e Kaloshin. Se houvesse infinitas configurações, elas formariam uma curva contínua de soluções quando as equações fossem estendidas aos números complexos. Seguindo essa curva “até o infinito”, as distâncias entre os corpos teriam de se comportar de maneiras que se cancelam num equilíbrio preciso. Os corpos se aproximam de um de dezesseis diagramas limite identificados por Albouy e Kaloshin, cada um impondo condições sobre as massas.
O novo trabalho torna essas condições exatas para toda massa positiva e descarta os casos problemáticos um por um:
- configurações em que quatro corpos formam um aglomerado compacto do qual o quinto se aproxima são excluídas expandindo a energia potencial — que permanece constante ao longo da curva — em ordens cada vez mais altas; para massas positivas, as condições resultantes se contradizem;
- prova-se que outros dois diagramas nunca ocorrem;
- para todo o resto, o autor descreve todas as condições compatíveis sobre as massas com álgebra computacional exata — 2.206 sistemas algébricos — e, para cada um, produz um certificado numérico: uma lista de números racionais cujas propriedades, verificadas em aritmética exata, provam que o equilíbrio é impossível.
Uma armadilha armada pelas massas negativas
Há um obstáculo que a álgebra pura não consegue contornar. Outro matemático, Roberts, havia encontrado infinitas configurações centrais para as massas (1, 1, 1, 1, −¼) — com uma massa negativa. Trocando alguns sinais, isso se transforma em infinitas soluções das equações complexificadas para as massas (4, 4, 4, 4, 1). Não são configurações reais, mas um argumento que só enxerga as equações complexas não consegue distingui-las.
Assim, nessas massas, e na razão relacionada (1, 1, 4, 4, 4), o autor conta diretamente as configurações reais, com uma busca por computador que usa aritmética intervalar garantida:
- para as massas (1, 4, 4, 4, 4): 306 configurações a menos de rotação e mudança de escala — 60 em linha reta, 24 formando um pentágono convexo, e as demais com um ou dois corpos no interior;
- para (1, 1, 4, 4, 4): 294.
As 60 em linha reta coincidem com uma contagem anterior de Moulton.
Verificado por máquina
Uma prova que repousa sobre tantos cálculos precisa de uma verificação robusta. Cada certificado foi reverificado por um programa separado, escrito a partir das definições do artigo. Acima de tudo, o teorema é provado no assistente de provas Lean 4, um programa que verifica cada passo lógico. A prova formal nem sequer pressupõe os resultados de Albouy e Kaloshin: ela rededuz o que precisa, encontrando por busca 1.376 diagramas rotulados que satisfazem as regras deles. Ela é aceita por outros dois verificadores independentes de provas em Lean. Compilá-la do zero leva cerca de 860 horas de CPU.
O artigo termina com uma breve declaração: ferramentas de IA generativa foram usadas para encontrar e provar os resultados, escrever os programas e a formalização em Lean, e redigir o texto. As ferramentas não são nomeadas.
O que o resultado diz e o que não diz
O resultado diz respeito a cinco corpos num plano. Prova que o número de configurações é finito para qualquer conjunto de massas positivas, mas dá contagens exatas apenas nas poucas razões de massas estudadas.