Исследователи Microsoft Research доказали гипотезу Каннана — Ловаса — Симоновитса (KLS), сформулированную в 1995 году. Над решением работали Чжао Сун и Синьчжи Чжан, которые использовали ИИ-агентов для проверки промежуточных рассуждений и анализа более 100 вариантов решения задачи.
Гипотеза KLS описывает геометрию многомерных выпуклых тел и эффективность их разрезов. Утверждается, что разница между лучшим плоским разрезом и оптимальным разрезом произвольной формы ограничена постоянным числом, не зависящим от размерности пространства. Это важно для алгоритмов случайной выборки.
ИИ помогал ученым выполнять вычисления с тензорами высокого порядка и параллельно исследовать различные математические направления. Исследователи итеративно отбирали перспективные критерии, отбрасывая неудачные идеи. Решающую роль сыграло сочетание работы агентов с математической интуицией авторов.
Ключевым этапом стало рекурсивное применение найденного критерия, позволившее доказать, что суммарный вклад ошибок остается ограниченным независимо от размерности. Доказательство было формализовано в системе Lean 4, что обеспечило высокую степень строгости результатов.
