dxdt.blog: занимательный интернет-журнал

В декабре 2024 года я писал на dxdt, что эффективным направлением применения ИИ-LLM к математическим задачам был бы поиск контрпримеров к более или менее известным утверждениям, в формате компьютерного доказательства. В качестве примера сборников подходящих задач я приводил “Коуровскую тетрадь” (это широко известный в узких кругах канонический список задач теории групп). Цитата из той записки:

Для заметной части из этих проблем и связанных задач можно было бы отыскать контрпримеры (и даже просто – примеры), используя современные возможности по оптимизированному перебору текстов компьютерных доказательств.
[…]
То есть, это самое реальное применение для знаменитых “LLM с нейросетками” на ближайшее время, при котором они могли бы оказаться очень эффективными для математических исследований.

Ну, идея довольно очевидная, поэтому, кто бы сомневался, что именно так и вышло: на днях OpenAI опубликовали список из десяти достаточно известных математических проблем, к которым предложены решения или контрпримеры, найденные “методами ИИ”, с использованием Lean.

Интересно, что одна из решённых в OpenAI задач – прямо указана и в “Коуровской тетради”, но лишь в самой свежей, 21-й редакции (я проверил только для англоязычной версии, понятно). В публикации OpenAI – это третья глава с утверждением non-sofic groups exist и контрпримером – с построением такой группы. В англоязычной “Коуровской тетради” это задача 21.86. Да, там обратная формулировка: “всякая ли группа является софической (sofic)?”. Но это как раз то, что нужно для поиска контрпримера: покажите одну группу, которая non-sofic, и это даст ответ – нет, не всякая. (“Софической”, конечно, не лучший перевод – должно быть “терминальной” или “терминируемой”, но данный вариант уже занят.)

Но что особенно занятно, так это то, что решённая ИИ OpenAI задача 21.86 в тетрадь добавлена в этом же, 2026 году! Удивительное совпадение. Например, препринт на Arxiv с 21-м изданием, в котором появляется данная задача, датирован январём 2026 года (версия 39, кому интересно). Естественно, сама исходная гипотеза про “софичность” всех групп – сильно старше, она, примерно, 2000 года. Однако в более старых версиях “Коуровской тетради” она не указана, а, похоже, появляется только в 2026 году.

Адрес записки: https://dxdt.blog/2026/08/12/18863/