Десять агентов Claude Sonnet 5.5 за 15 часов доказали задачу Томсона для N=7 в Lean

Компания Vals AI дала десяти агентам Claude Sonnet 5.5 на максимальном усилии общий Lean-проект и доску сообщений. За примерно 15 часов без вмешательства человека они написали формальное доказательство задачи Томсона для семи зарядов. Результат — один файл Solution.lean на 17 895 строк, импортирующий только Mathlib.

Обе целевые теоремы зафиксировали заранее в challenge-файле: регулярная пятиугольная бипирамида даёт наименьшую кулоновскую энергию, и любой минимум совпадает с ней с точностью до вращений, отражений и перенумерации. Энергия бипирамиды равна 14.4529774142…. Доказательство разбивает все конфигурации по наименьшему попарному скалярному произведению m. При m ≥ −0.90 работает полуопределённый сертификат степени 5 по методу Бахок–Валлентена в энергетической версии Кона–Ву, дающий запас 3×10⁻⁴. При m < −0.90 пять «ломтиков» на отрезке [−0.99, −0.90] закрывают отдельные трёхточечные сертификаты, а остаток при m ≤ −0.99 добивается интервальной арифметикой и точным аргументом второго порядка, который заодно даёт единственность. Численные сертификаты, найденные SDP-решателем, округлены до точных чисел и перепроверены ядром Lean.

Проверок пять: чистая сборка Lean (599 секунд, из них lake build 344 секунды, 8 928 задач), отчёт об аксиомах (только propext, Classical.choice, Quot.sound), компаратор соответствия зафиксированным формулировкам, экспорт в nanoda, независимую реализацию ядра, принявшую все 47 854 декларации, и негативный контроль. Изменение одного целого числа в данных сертификата заставило nanoda отвергнуть доказательство.

За 15 часов агенты обменялись 1270 сообщениями; стартовый бриф предлагал девять направлений, включая перенос метода N=8. Случай N=8 опубликовали 18 сентября 2026 года Кривонос, Лир и Тейлор, Lean-разработку выполнили Тоби-Смит и Зугейд. Для N=5 понадобилось компьютерное доказательство Шварца. Исходники, скрипты проверок и логи выложены на GitHub.