ИИ-ассистент за день разобрал 1072 задачи по теории групп и, возможно, решил одну из них
Команда разработчиков ИИ-сотрудника сообщила, что её система за один день прошла по всем 1072 нерешённым задачам 21-го выпуска Коуровской тетради и получила результат по одной из них, задаче 20.87. Решение пока не проверено людьми: препринт 18 октября отправлен редакторам сборника в Новосибирск, ответа ещё нет, а код и текст выложены в открытом репозитории на GitHub.
Речь идёт о проекте ИИ-сотрудника, который ведёт задачи в компании, пишет код и отвечает в чатах. В октябре его авторы решили проверить, справится ли система с работой, где правильный ответ заранее никому не известен и где модель нельзя «заболтать»: в открытой математической задаче результат либо есть, либо его нет. Первой целью была задача Рингеля о раскраске карт «Земля-Луна» в ветке Гетнера и Суланке, где требовался граф из двух плоских слоёв с долей независимых вершин меньше 2/17. Поиск быстро находил известные рекорды на 17 и 25 вершинах, 16 октября нашёлся граф на 33 вершинах, и отдельный скрипт подтвердил, что обе его части плоские. Однако на 34 и 35 вершинах процесс встал: отжиг застревал на лишних пятёрках, а точный поиск через SAT-решатель перебрал более 1200 окрестностей лучшей точки без результата, при оценке полного перебора одного из соседних случаев примерно в 30 процессор-лет. 18 октября эту линию поставили на паузу.
Из неудачи команда сделала вывод: задачи, которые решаются перебором, давно перебирают люди с кластерами, и соревноваться с ними в ядро-часах бессмысленно. Нужна была задача, где работает рассуждение, а компьютер только проверяет. Такой площадкой стала Коуровская тетрадь — сборник нерешённых задач теории групп, который ведут в Новосибирске с 1965 года и переиздают каждые несколько лет, отмечая решённые задачи со ссылкой на автора. Из 21-го выпуска команда насчитала 1072 задачи без решения и без отметок о том, что их уже трогали ИИ. Отбор шёл в несколько слоёв: тетрадь порезали на шесть частей, разные модели прошлись по каждой, отмечая задачи, которые можно продвинуть за день, затем на машине собрали GAP 4.14 и прогнали быстрые проверки на контрпримеры по библиотекам групп. Часть задач на этом отвалилась, а по одной (21.100) выяснилось, что ответ уже опубликован летом на arXiv. В глубокую работу ушли восемь задач, каждая в своей параллельной сессии: 20.87 решена полностью, по 21.23(b) ответ получен и независимая проверка на 15 простых группах расхождений не нашла, по 20.21 показано отсутствие примеров порядка меньше 3072, но это не решение, по 21.2 доказано «да» для нескольких семейств и простых групп до 2·10⁶ без общего ответа, а 21.90, 20.51 и 20.52 продвинулись, но не закрыты.
Задача 20.87, поставленная китайским алгебраистом Ши Вуцзе, касается конечных групп, у которых порядок любого элемента делится не более чем на два разных простых числа: 12 = 2·2·3 подходит, а 30 = 2·3·5 уже нет. Вопрос в том, из каких простых «атомов» могут собираться такие группы. Случай одного простого числа разобран давно и даёт конечный список, а для двух ответа в литературе команда не нашла. Первый шаг почти бесплатный: свойство наследуется подгруппами и факторгруппами, поэтому атом хорошей группы сам хороший, а хорошая простая группа сама себе пример, и задача сводится к вопросу, какие простые группы обладают этим свойством. Поскольку все конечные простые группы известны, дальше нужно аккуратно пройти по их списку, и именно здесь начинается основная работа. Ответ поместился на одну схему: семь знакопеременных групп, 13 спорадических из 26, пять семейств, где всё решает арифметика числа q, и 18 отдельных групп лиева типа. Наиболее наглядная часть — знакопеременные: чтобы получить элемент порядка 30, нужны одновременно цикл длины 3, цикл длины 5 и «двойка», которую в чётной перестановке приходится брать парой транспозиций, то есть ещё четыре предмета; в A₁₂ двенадцати предметов хватает, в A₁₁ уже нет. С семействами сложнее: например, L₂(q) входит в ответ, когда у чисел рядом с q, точнее у (q±1)/d, мало простых делителей, и с ростом q таких значений становится всё меньше. Бесконечны ли эти пять семейств, команда не знает — это вопрос аналитической теории чисел, но для ответа на 20.87 он не нужен, поскольку условие на q записано явно.
Проверка строилась так, чтобы одна и та же ошибка не прошла дважды. Доказательство написано текстом: сведение к простым группам, разбор знакопеременных и спорадических, общее рассуждение для групп лиева типа через максимальные торы, сведение к полям из 2, 3, 4 и 8 элементов и разбор оставшегося. Каждый вывод затем сверяли с компьютером разными способами. Главная проверка простая и злая: в GAP есть библиотека таблиц характеров ctbllib с 154 простыми группами, из таблиц видны порядки всех элементов, то есть свойство проверяется напрямую, без теории. Теорема для каждой из 154 групп говорит «входит» или «не входит», и сравнение дало 85 групп со свойством и 69 без него — теорема угадала все 154. Отдельно формулы для семейств сравнили с прямым счётом (L₂(q) до q = 2000 и другие, более 400 групп), метод торов против таблиц на 54 группах и классы сопряжённости настоящих матричных групп там, где таблиц нет. Самую тонкую группу G₂(8), отсутствующую в библиотеке, построили заново и проверили на 3000 случайных элементах. Ещё одна сессия получила только формулировку и текст решения и читала его как рецензент, со своим кодом и без доступа к рассуждениям команды, и ошибок не нашла; вручную сверены 39 групп из ответа. Все материалы лежат в репозитории github.com/AutoPasha/kourovka-20-87, а проверку по таблицам можно повторить двумя командами в GAP.
Контекст этой истории шире одной задачи. ИИ-ассистенты всё чаще получают доступ к инструментам: в статье о tool calling на Go разбирается, почему валидный вызов функции ещё не означает разрешения на операцию, и это напоминает о границах автономности. В проекте с Коуровской тетрадью граница проведена жёстко: система рассуждает и проверяет, но окончательный вердикт остаётся за людьми и редакторами. Похожий подход виден в другом материале потока — про радар спроса, где ИИ-классификатор отсеивает мусор и оценивает находки, а отвечает заказчику человек. Общая логика такова: модель ускоряет перебор вариантов и черновую проверку, но ответственность за результат не передаётся. Для российского рынка это ещё и сигнал о зрелости локальных команд, которые строят агентные системы не только под бизнес-задачи, но и под исследовательские сценарии с воспроизводимым кодом и открытыми данными.
Сравнение с альтернативами напрашивается само. Классический перебор на кластере, как в случае задачи Рингеля, требует десятков процессор-лет и не даёт рассуждения, а чистая генерация текста без проверки в математике бесполезна, поскольку её нельзя верифицировать. Подход команды занимает промежуточное положение: рассуждение модели плюс независимая компьютерная проверка на библиотеках групп и повторный «рецензентский» проход другой сессией. Слабое место — зависимость от качества формализации: если условие задачи переписано неточно, проверка подтвердит неверную теорему. Именно поэтому авторы подчёркивают, что решение 20.87 пока не проверено людьми, а препринт отправлен редакторам Коуровской тетради 18 октября и ответа ещё нет.
Дальше всё зависит от реакции редакторов и математического сообщества. Если ошибка есть, команда хочет узнать о ней раньше редакторов, и открытый репозиторий с кодом проверки как раз для этого. Если решение подтвердится, это станет заметным прецедентом: ИИ-система за день прошла по 1072 открытым задачам, довела до результата одну и получила частичные продвижения ещё по нескольким. Открытыми остаются вопросы об устойчивости метода на задачах без конечного объекта проверки, о том, как оценивать вклад модели и человека, и о том, станут ли подобные проходы по сборникам нерешённых задач регулярной практикой. Пока же итог сдержанный: результат есть, проверка продолжается, а окончательный ответ даст не репозиторий, а рецензенты.