CINQ CORPS, UN NOMBRE FINI DE DANSES PARFAITES

Imaginez quelques étoiles ou planètes disposées si précisément que tout le groupe peut tourner comme un objet rigide, sans changer de forme. Pour cela, l’attraction gravitationnelle sur chaque corps doit pointer exactement vers le centre de masse du groupe, avec une force proportionnelle à sa distance à ce centre. On appelle ces dispositions des configurations centrales. Ce sont les formes des solutions particulières du problème à n corps dans lesquelles les corps gardent le même motif relatif, dont les équilibres relatifs qui tournent d’un bloc.

Si un motif convient, toute copie tournée, agrandie ou déplacée convient aussi : les mathématiciens les comptent donc « à similitude près ».

Le sixième problème de Smale

La question se pose simplement : pour tout choix de masses positives, le nombre de configurations centrales est-il fini ? C’est le sixième problème d’une liste de problèmes ouverts dressée par le mathématicien Smale.

Voici où l’on en était, selon l’article :

• Trois corps : exactement cinq — les deux triangles équilatéraux de Lagrange et les trois alignements d’Euler.
• Quatre corps : la finitude a été démontrée par Hampton et Moeckel, pour toutes les masses positives.
• Cinq corps dans un plan : Albouy et Kaloshin ont démontré la finitude en 2012, mais seulement pour des masses hors d’un ensemble exceptionnel — une mince famille de combinaisons de masses définies par des équations polynomiales, où leur raisonnement ne passait pas.

Refermer l’ensemble exceptionnel

Tejasvi Singh Tomar supprime cet ensemble exceptionnel. Le théorème principal : pour tout choix de cinq masses positives, le problème plan à cinq corps a un nombre fini de configurations centrales à similitude près.

La stratégie suit celle d’Albouy et Kaloshin. S’il y avait une infinité de configurations, elles formeraient une courbe continue de solutions une fois les équations étendues aux nombres complexes. En suivant cette courbe « vers l’infini », les distances entre les corps doivent se comporter de façon à se compenser dans un équilibre précis. Les corps s’approchent alors de l’un des seize diagrammes limites identifiés par Albouy et Kaloshin, chacun imposant des conditions aux masses.

Le nouveau travail rend ces conditions exactes pour toute masse positive, et élimine les cas gênants un à un :

• les configurations où quatre corps forment un amas serré dont s’approche le cinquième sont exclues en développant l’énergie potentielle — constante le long de la courbe — à des ordres de plus en plus élevés ; pour des masses positives, les conditions obtenues se contredisent ;
• deux autres diagrammes ne se produisent jamais ;
• pour tout le reste, l’auteur décrit toutes les conditions de masse compatibles par calcul formel exact — 2 206 systèmes algébriques — et produit pour chacun un certificat numérique : une liste de nombres rationnels dont les propriétés, vérifiées en arithmétique exacte, prouvent que l’équilibre est impossible.

Un piège tendu par des masses négatives

Il reste une difficulté que l’algèbre seule ne peut pas contourner. Un autre mathématicien, Roberts, avait trouvé une infinité de configurations centrales pour les masses (1, 1, 1, 1, −¼) — dont une masse négative. En changeant certains signes, cela donne une infinité de solutions des équations complexifiées pour les masses (4, 4, 4, 4, 1). Ce ne sont pas de vraies configurations, mais un raisonnement qui ne voit que les équations complexes ne peut pas les distinguer.

Pour ces masses, et pour le rapport voisin (1, 1, 4, 4, 4), l’auteur compte donc directement les configurations réelles, par une recherche informatique en arithmétique d’intervalles garantie :

• pour les masses (1, 4, 4, 4, 4) : 306 configurations à rotation et changement d’échelle près — 60 alignées, 24 formant un pentagone convexe, les autres avec un ou deux corps à l’intérieur ;
• pour (1, 1, 4, 4, 4) : 294.

Les 60 alignées concordent avec un décompte antérieur de Moulton.

Vérifiée par la machine

Une preuve qui repose sur autant de calculs exige une vérification solide. Chaque certificat a été revérifié par un programme distinct, écrit à partir des définitions de l’article. Surtout, le théorème est démontré dans l’assistant de preuve Lean 4, un logiciel qui contrôle chaque étape logique. La preuve formelle ne suppose même pas les résultats d’Albouy et Kaloshin : elle redémontre ce dont elle a besoin, en trouvant par une recherche 1 376 diagrammes étiquetés qui satisfont leurs règles. Elle est aussi acceptée par deux autres vérificateurs indépendants de preuves Lean. La reconstruire depuis zéro demande environ 860 heures de calcul.

L’article se termine par une courte mention : des outils d’IA générative ont servi à trouver et démontrer les résultats, à écrire les programmes et la formalisation Lean, et à rédiger le texte. Les outils ne sont pas nommés.

Ce qu’il dit, et ce qu’il ne dit pas

Le résultat porte sur cinq corps dans un plan. Il prouve que le nombre de configurations est fini pour tout ensemble de masses positives, mais ne donne de décomptes exacts que pour les quelques rapports de masses étudiés.