22 УМНОЖЕНИЯ, И НИ ОДНИМ МЕНЬШЕ
Конфликт интересов. Авторы указывают, что ИИ-агенты — Claude от Anthropic — под их руководством написали поисковый код и те доказательства на Lean, которые не требуют проверки человеком, тогда как часть, которую должен проверить человек, разработали сами авторы. Эта статья также написана Claude.
Перемножение двух квадратных таблиц чисел — матриц — школьным способом требует n³ умножений для таблиц из n строк и n столбцов. Штрассен показал, что две матрицы 2 × 2 можно перемножить за 7 умножений вместо 8. Трюк можно применять рекурсивно: разрезать большую матрицу на четыре блока, рассматривать каждый блок как одно число и повторять. Тогда затраты растут как n^2,807 вместо n³. Согласно статье, оптимальность этого рецепта для 2 × 2 была доказана в 1971 году.
Та же идея работает для любого фиксированного размера. Рецепт, который перемножает две матрицы 3 × 3 за r умножений и по-прежнему работает, когда элементы являются блоками, даёт затраты, растущие как n в степени log₃ r. Простая арифметика показывает, что на кону: такой рецепт обходит Штрассена ровно тогда, когда r не больше 21, и проигрывает при 22 и более. Лучший известный рецепт для 3 × 3, принадлежащий Ладерману, использует 23 умножения и не улучшался с 1976 года.
Дверь, остававшаяся приоткрытой
Наилучшее возможное число для данной задачи называется её рангом. Нижние оценки ранга умножения 3 × 3 медленно ползли вверх: 19 в 2003 году, затем 20 в марте 2026 года, вычисленная Ваном над крошечной системой чисел, где есть только 0 и 1 и где 1 + 1 = 0. В сентябре 2026 года Ван и команда под руководством Яна независимо друг от друга достигли 21 с разницей в десять дней. Но 21 всё ещё оставляла место для рецепта 3 × 3, более быстрого, чем у Штрассена.
Исаак Рудич из Политехнической школы Монреаля и Университета Карнеги — Меллона и Луи-Мартен Руссо из Политехнической школы Монреаля теперь подняли оценку до 22.
Теорема 1. Любой алгоритм, который перемножает две матрицы 3 × 3 с целочисленными константами и может применяться рекурсивно к блокам любого размера, использует не менее 22 умножений.
Значит, никакой такой алгоритм не может быть лучше примерно n^2,814 — и ни один не может обойти метод Штрассена для 2 × 2.
496 задач поменьше
Доказательство опирается на таблицу, разработанную Ваном, которая разбивает трудную задачу на 496 более лёгких. Каждая из них добавляет к первой матрице «условия» — например, что определённые её элементы в сумме дают ноль. Чем больше условий, тем легче задача, вплоть до тривиального случая, когда матрица целиком состоит из нулей.
Сначала авторы построили точную поисковую программу, которая сообщала им истинный ответ для каждой задачи до того, как они пытались его доказать. Эти ответы служили картой: они показывали, за какими нижними оценками стоит гнаться. В итоге их доказательство даёт оценки для всех 496 задач, решает 359 из них точно — против 195 в последних результатах Вана — и повышает нижнюю оценку для 252. Их собственная теорема о «склейке» объединяет рецепты для двух более лёгких задач в рецепт для третьей и дала 145 верхних оценок.
В итоговой формулировке важны два условия. Целочисленные константы: рецепт с целочисленными константами, прочитанный в системе чисел из 0 и 1, остаётся корректным рецептом без лишних умножений, поэтому оценка переносится. Блоки: без этого требования существуют обходные пути. Алгоритм Росовски для 3 × 3, цитируемый в статье, требует лишь 21 умножения, но опирается на коммутативность чисел и не может применяться рекурсивно.
Доказательство, проверенное машиной
Доказательство написано на Lean — языке программирования, в котором теорема компилируется, только если каждый шаг проверен. Полное доказательство занимает около миллиона строк в 3521 модуле, и его проверка длится 11,1 часа на одном ядре процессора. Читать его целиком никому не нужно. Проверяющий читает библиотеку примерно из 1000 строк, написанную авторами ещё до появления какого-либо доказательства, которая определяет, что такое рецепт умножения, и формулирует теорему; остальное проверяет ядро Lean, а независимый проверяющий инструмент может воспроизвести результат.
Авторы также отмечают, что ИИ-агенты искали литературу: они проверили, что каждый источник существует, «но не то, что в каждом содержится именно та идея, которую мы ему приписываем».
Последний зазор
Остаётся один вопрос: существует ли рецепт для 3 × 3 с 22 умножениями, или 23 Ладермана — истинный минимум? Авторы ожидают, что зазор «будет закрыт в ближайшее время», и опубликуют свой поисковый код, как только это произойдёт или как только статья будет принята к публикации. Кроме того, оценка не охватывает рецепты с нецелыми константами.
