Как ИИ-сотрудник за день прошёл по 1072 открытым задачам теории групп и одну, кажется, решил

Сразу о главном, чтобы первый же комментарий не начинался с вопроса «а кто проверял». Людьми решение пока не проверено. Письмо с препринтом ушло редакторам Коуровской тетради в Новосибирск 18 октября, ответа еще нет. Код проверки и препринт лежат в открытом репозитории: github.com/AutoPasha/kourovka-20-87. Если там ошибка, мы хотим узнать о ней раньше редакторов.

Дальше про то, как мы туда пришли, и про то, почему сначала ничего не получилось.

Сначала была Земля и Луна

Мы делаем ИИ-сотрудника: он ведет задачи в компании, пишет код, отвечает в чатах. В октябре захотелось проверить, вытянет ли он работу, где правильный ответ никому не известен заранее и где его нельзя заболтать. Открытая математическая задача подходит идеально, потому что тут либо есть проверяемый результат, либо его нет.

Первой целью была задача Рингеля о раскраске карт «Земля-Луна», точнее ее ветка у Гетнера и Суланке: нужен граф из двух плоских слоев, у которого доля независимых вершин меньше 2/17. Для этого хватило бы графа на 35 вершинах без независимой пятерки. Поиск мы собрали быстро, он за секунды находил известные рекорды на 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 групп из ответа.

Все это лежит в репозитории, проверку по таблицам повторить можно двумя командами:

gap -q scan_ctbllib.g < /dev/null > scan_ctbllib.out
python3 compare_theorem_with_tables.py

Чего мы не знаем

Машинная проверка ловит неверный ответ на конечном куске, но не ловит дыру в рассуждении про бесконечные семейства. Сто пятьдесят четыре совпадения из ста пятидесяти четырех убеждают нас, но не рецензента, и правильно делают. Поэтому решение ушло в тетрадь как препринт с оговоркой «не проверено людьми», а не как новость.

Еще мы не знаем, насколько задача была трудной для специалиста. Возможно, эксперт по группам лиева типа закрыл бы ее за неделю, просто руки не дошли. Нам интересно другое: сотрудник сам выбрал ее из тысячи, довел до конца и проверил так, что результат можно пересчитать без него.

Если вы занимаетесь конечными группами и найдете ошибку, напишите в issues репозитория. Мы перескажем это в следующем тексте, когда придет ответ из Новосибирска.

Препринт на английском и русская версия: github.com/AutoPasha/kourovka-20-87