ИИ-система предложила решение задачи Коуровской тетради по теории групп
Habr AI · оригинал
Материал подготовлен автоматизированной редакционной системой. Факты можно сверить по указанному первоисточнику.
Команда разработчиков применила ИИ-агента к нерешенной задаче из 21-го выпуска Коуровской тетради, предложив полное решение для случая двух простых делителей порядков элементов. Препринт с доказательством и кодом проверки передан редакторам в Новосибирске, где ожидается независимая верификация математиков.
Случай демонстрирует переход ИИ от генерации кода к решению открытых научных задач с формальной проверкой, что меняет парадигму автоматизации фундаментальных исследований.
Команда разработчиков, создающая ИИ-сотрудника для корпоративных задач, провела эксперимент по решению открытых математических проблем. Первоначально система пыталась атаковать задачу Рингеля о раскраске карт «Земля-Луна», но столкнулась с вычислительными ограничениями: перебор вариантов требовал бы около 30 процессор-лет, что сделало подход неэффективным. Это привело к выводу, что для ИИ более перспективны задачи, где ключевую роль играет логическое рассуждение, а компьютер служит лишь инструментом верификации.
В качестве новой цели был выбран 21-й выпуск Коуровской тетради — сборника нерешенных задач теории групп, издаваемого в Новосибирске с 1965 года. Из 1072 открытых задач ИИ отобрал восемь кандидатов для глубокой работы. Наиболее значимым результатом стало полное решение задачи 20.87, поставленной китайским алгебраистом Ши Вуцзе. Вопрос касался структуры конечных групп, где порядок любого элемента делится не более чем на два различных простых числа.
Доказательство сводит проблему к классификации простых групп. Ответ включает семь знакопеременных, 13 спорадических и 18 отдельных групп лиева типа, а также пять семейств, зависящих от арифметики параметра q. Для проверки корректности разработчики использовали библиотеку GAP 4.14 и таблицы характеров ctbllib. Система сверила теоретические выводы с данными по 154 простым группам: 85 из них обладают требуемым свойством, 69 — нет, и теорема совпала с фактами во всех случаях.
Дополнительно проводились независимые проверки: сравнение формул для семейств с прямым подсчетом на более чем 400 группах, а также анализ случайных элементов в группе G₂(8), отсутствующей в стандартных базах. Отдельная сессия ИИ выступала в роли рецензента, проверяя логику доказательства без доступа к исходным рассуждениям. Несмотря на успех машинной верификации, авторы подчеркивают, что решение не проверено людьми и может содержать ошибки в рассуждениях о бесконечных семействах.
Препринт с решением и кодом проверки опубликован в открытом репозитории GitHub и направлен редакторам Коуровской тетради 18 октября. Авторы приглашают специалистов по конечным группам проверить работу через issues репозитория, отмечая, что независимая экспертиза необходима для подтверждения вклада ИИ в фундаментальную математику.