ИИ-агенты помогли доказать гипотезу KLS — головоломку из геометрии, которую не могли решить 31 год

Гипотеза Каннана — Ловаса — Симоновица (KLS) — одна из ключевых открытых задач геометрии высоких размерностей: можно ли для широкого класса многомерных распределений приблизить лучший способ «разрезать» пространство плоским сечением почти так же эффективно, как сечением произвольной формы, с разрывом, ограниченным универсальной константой, не зависящей от размерности. От ответа зависит, насколько быстро случайные алгоритмы исследуют сложные многомерные данные — вопрос, важный далеко за пределами чистой математики, в том числе для статистики и машинного обучения. Гипотеза стояла нерешённой с 1995 года.

Что сделали ИИ-агенты, а что — люди

21 октября Microsoft Research опубликовала подробный разбор работы исследователя Синьчжи Чжана и соавтора Чжао Суна. ИИ-агенты вели параллельный перебор: проверяли больше сотни кандидатных подходов, доводили до конца громоздкие тензорные вычисления, готовили черновики выкладок и прогоняли внутренние проверки доказательства. Но направление поиска, отбор перспективных веток среди неудачных и — главное — сам рекуррентный метод вместе с доказательством того, что накопленная погрешность остаётся ограниченной, авторы называют своим собственным вкладом: именно эту идею, а не перебор агентов, независимая группа математиков впоследствии назвала решающим шагом.

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

Независимая проверка

Препринт Microsoft появился на arXiv в начале октября; версия с полным доказательством вышла 4 октября. В том же окне отдельная группа математиков опубликовала собственное полное доказательство, прямо назвав ключевой критерий из первой версии работы Суна и Чжана решающим шагом, а вскоре появилось и третье доказательство на близкой идее. Результат также формализован в системе Lean 4 — ещё один штрих к растущей практике машинной проверки математических доказательств наравне с перебором подходов нейросетями.

Что это значит на практике

Прямого эффекта на доступность сервисов из России здесь нет — это открытая научная публикация, а не платный продукт: препринт на arXiv и разбор Microsoft Research доступны без ограничений по геолокации. Практический вывод для тех, кто сам пробует применять ИИ-агентов к сложным задачам — не только математическим, но и инженерным, аналитическим, исследовательским, — в другом: кейс лишний раз подтверждает, что одной подсказки «реши это» флагманской модели недостаточно даже с большим бюджетом токенов. Рабочая схема — декомпозиция на части, параллельный перебор вариантов агентами и обязательная проверка человеком на каждом шаге, а не ожидание, что система выдаст готовый результат с первой попытки.