17 895 строк за 15 часов: агенты Claude закрыли задачу Томсона для семи зарядов

Один лишний факт о числе 17 895. Столько строк занимает Lean-доказательство, которое десять агентов Claude Sonnet 5.5 написали за 15 часов автономной работы, — и которое закрывает вопрос, стоявший открытым со времён Джозефа Джона Томсона, то есть с 1904 года.

Задача, которую все «знали», но никто не доказал

Формулировка задачи Томсона умещается в одно предложение: как разместить N одинаковых зарядов на сфере, чтобы энергия их взаимного отталкивания была минимальной? Для семи зарядов компьютерный перебор десятилетиями выдавал один и тот же ответ — пятиугольная бипирамида: пять точек на экваторе, по одной на полюсах.

Проблема в слове «доказать». Пространство конфигураций непрерывно, и чтобы закрыть вопрос, нужно строго исключить бесконечное множество альтернативных расстановок. Точные решения известны лишь для нескольких малых N: случай N=5 потребовал компьютерного доказательства Шварца, а N=8 был закрыт только в сентябре 2026-го — компьютерной работой Кривоноса, Лира и Тейлора с последующей Lean-формализацией Тоби-Смита и Зугейда. Семёрка при этом оставалась дырой.

Доска объявлений, десять агентов и интегратор

Компания Vals AI поставила эксперимент с почти демонстративно простой инфраструктурой: десять агентов Sonnet 5.5 на максимальном усилии, общий Lean-проект, доска сообщений для координации — и 15 часов без вмешательства человека. Целевые теоремы были зафиксированы заранее в challenge-файле: минимальность бипирамиды и единственность минимума с точностью до вращений, отражений и перенумерации.

Стартовый бриф предлагал девять направлений атаки — от переноса метода N=8 до построения верифицированного движка сертификатов. Агенты имели право отбрасывать и объединять направления, объясняя почему. За 15 часов они обменялись 1270 сообщениями; один из агентов взял на себя роль интегратора и сводил проверенные куски в единый файл Solution.lean.

Само доказательство устроено как аккуратная охота на исключения. Всякая конфигурация классифицируется по наименьшему попарному скалярному произведению: основной случай закрывается полуопределённым сертификатом степени 5 по методу Бахок—Валлентена в энергетической версии Кона—Ву, пограничная зона нарезается на пять «ломтиков» с отдельными сертификатами, а оставшаяся узкая шапка — там, где два заряда почти противоположны, — добивается интервальной арифметикой и точным аргументом второго порядка, который заодно даёт единственность. Все численные сертификаты, найденные SDP-решателем, округлены до точных чисел и перепроверены ядром Lean: доказательство не зависит от плавающей точки.

Пять проверок и одна диверсия

К верификации авторы подошли параноидально, и это, пожалуй, самая поучительная часть работы. Файл прогнали через пять независимых проверок: чистую сборку Lean (599 секунд), отчёт об аксиомах (только три стандартные), компаратор соответствия зафиксированным формулировкам, а затем — экспорт в nanoda, независимую реализацию ядра Lean, которая приняла все 47 854 декларации. Финальный штрих — негативный контроль: авторы намеренно изменили одно целое число в данных сертификата и убедились, что nanoda доказательство отвергает. Проверялка проверена.

Насколько это большое событие

Сообщество встретило результат со смесью восторга и отрезвляющих оговорок — и обе реакции по-своему справедливы. С одной стороны, «бесплатный ИИ успешно работает над нерешёнными задачами — это безумие», как сформулировал топ-комментарий в треде r/singularity. С другой — ответ был известен заранее, доказан лишь частный случай N=7, а не общая задача, и по чистой математической силе это скромнее сентябрьского N=8, метод которого агенты во многом переиспользовали.

Но значимость здесь не в конкретной теореме, а в методологии. Автономная команда агентов за ночь произвела математический результат публикационного качества с машинной верификацией каждого шага — без руководителя, без разметки, без человека в цикле. Неделей раньше Sonnet 5.5 удивляла бенчмарками, теперь она демонстрирует другой режим: не отвечать на вопросы, а неделями копать открытые проблемы. Если экономика такого копания сойдётся, очередь из недоказанных гипотез — а заодно из индустрий, которым нужна формальная верификация критического софта, — выстроится сама. Исходники, скрипты проверок и логи выложены на GitHub — редкий случай, когда «ИИ решил задачу» можно пересобрать у себя и проверить до последней строки.