ПЯТЬ ТЕЛ И КОНЕЧНОЕ ЧИСЛО ИДЕАЛЬНЫХ ТАНЦЕВ

Представьте несколько звёзд или планет, расставленных так точно, что вся группа может вращаться как жёсткий объект, не меняя формы. Для этого притяжение, действующее на каждое тело, должно быть направлено точно к центру масс группы, а его сила — пропорциональна расстоянию до центра. Такие расположения называют центральными конфигурациями. Это формы особых решений задачи n тел, в которых тела сохраняют одно и то же взаимное расположение, включая относительные равновесия, вращающиеся как целое.

Если какая-то фигура подходит, то подходит и любая её повёрнутая, увеличенная или сдвинутая копия, поэтому математики считают их «с точностью до подобия».

Шестая проблема Смейла

Вопрос формулируется просто: конечно ли число центральных конфигураций при любом выборе положительных масс? Это шестая проблема в списке открытых задач, составленном математиком Смейлом.

Вот как обстояли дела, по словам статьи:

• Три тела: ровно пять — два равносторонних треугольника Лагранжа и три прямые Эйлера.
• Четыре тела: конечность доказали Хэмптон и Мёккель для всех положительных масс.
• Пять тел на плоскости: Альбуи и Калошин доказали конечность в 2012 году, но лишь для масс вне исключительного множества — тонкого семейства сочетаний масс, заданного полиномиальными уравнениями, на котором их рассуждение ломалось.

Закрывая исключительное множество

Теджасви Сингх Томар устраняет это исключительное множество. Главная теорема: при любом выборе пяти положительных масс плоская задача пяти тел имеет конечное число центральных конфигураций с точностью до подобия.

Стратегия следует Альбуи и Калошину. Если бы конфигураций было бесконечно много, они образовали бы непрерывную кривую решений при расширении уравнений на комплексные числа. Если идти вдоль этой кривой «на бесконечность», расстояния между телами должны вести себя так, чтобы взаимно компенсироваться в точном балансе. Тела приближаются к одной из шестнадцати предельных диаграмм, выделенных Альбуи и Калошиным, и каждая из них накладывает условия на массы.

Новая работа делает эти условия точными для любых положительных масс и исключает проблемные случаи один за другим:

• конфигурации, в которых четыре тела образуют плотное скопление, а пятое к нему приближается, исключаются разложением потенциальной энергии — она постоянна вдоль кривой — до всё более высоких порядков; для положительных масс получающиеся условия противоречат друг другу;
• доказано, что ещё две диаграммы никогда не возникают;
• для всего остального автор описывает все совместимые условия на массы с помощью точной компьютерной алгебры — 2206 алгебраических систем — и для каждой строит числовой сертификат: список рациональных чисел, свойства которых, проверенные в точной арифметике, доказывают, что баланс невозможен.

Ловушка отрицательных масс

Есть препятствие, которое чистая алгебра обойти не может. Другой математик, Робертс, нашёл бесконечно много центральных конфигураций для масс (1, 1, 1, 1, −¼) — с одной отрицательной массой. Смена некоторых знаков превращает это в бесконечно много решений комплексифицированных уравнений для масс (4, 4, 4, 4, 1). Это не настоящие конфигурации, но рассуждение, которое видит только комплексные уравнения, не может их отличить.

Поэтому при этих массах и при родственном соотношении (1, 1, 4, 4, 4) автор пересчитывает настоящие конфигурации напрямую — компьютерным поиском с гарантированной интервальной арифметикой:

• для масс (1, 4, 4, 4, 4): 306 конфигураций с точностью до поворота и масштабирования — 60 на одной прямой, 24 образуют выпуклый пятиугольник, остальные — с одним или двумя телами внутри;
• для (1, 1, 4, 4, 4): 294.

60 прямолинейных конфигураций совпадают с более ранним подсчётом Мултона.

Проверено машиной

Доказательство, опирающееся на такое количество вычислений, требует серьёзной проверки. Каждый сертификат перепроверила отдельная программа, написанная по определениям из статьи. Главное же — теорема доказана в системе доказательств Lean 4, программе, которая проверяет каждый логический шаг. Формальное доказательство даже не предполагает результаты Альбуи и Калошина: оно заново выводит всё необходимое, находя поиском 1376 помеченных диаграмм, удовлетворяющих их правилам. Его принимают ещё две независимые программы проверки доказательств Lean. Сборка с нуля занимает около 860 процессорных часов.

Статья завершается кратким заявлением: генеративные ИИ-инструменты использовались, чтобы найти и доказать результаты, написать программы и формализацию на Lean, а также подготовить черновик текста. Названия инструментов не приводятся.

Что сказано и что нет

Результат касается пяти тел на плоскости. Он доказывает, что число конфигураций конечно для любого набора положительных масс, но точные подсчёты даёт лишь для немногих изученных соотношений масс.