ИИ-сотрудник за один день разобрал 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

 

Источник