Триумф формальной логики. Нейросеть нашла математическое доказательство, которое люди не замечали 30 лет

Искусственный интеллект снова влез в математику, но на этот раз история оказалась чуть сложнее, чем выглядела в заголовках. Модель Aristotle от стартапа Harmonic формально доказала одну из задач из знаменитого списка проблем Пала Эрдеша. В соцсетях тут же появились восторженные посты про "ИИ, обошедший Эрдеша и Грэма". А потом математики разобрались в деталях и выяснили, что все немного тоньше: решена упрощенная версия задачи, а исходная, более сильная формулировка по-прежнему открыта.

Пал Эрдеш был одним из самых продуктивных математиков XX века. Он написал больше тысячи четырехсот статей, почти всегда в соавторстве, и обожал собирать красивые нерешенные задачи. Эти задачи из теории чисел, комбинаторики и теории графов много лет сводят с ума профессионалов и любителей. После смерти Эрдеша появился онлайн-сайт, который аккуратно каталогизирует "проблемы Эрдеша", отслеживает ссылки на статьи и меняет статус задач, когда те удается решить.

Задача номер 124 из этого списка относится к теории чисел. Интуитивно ее можно описать так. Берем несколько натуральных чисел и смотрим на все их степени: например, для набора 3, 4, 5 получаются последовательности 3, 9, 27, 81..., 4, 16, 64..., 5, 25, 125... Если отсортировать все эти числа по возрастанию, получится один общий список. В исходной работе 1996 года Эрдеш и соавторы спрашивали: можно ли для подходящих наборов чисел представить любое достаточно большое целое число как сумму различных элементов из такого списка. Чтобы у задачи вообще был шанс на положительный ответ, на набор накладываются два условия: не все числа должны иметь общий делитель больше единицы и должна выполняться определенная сумма вида 1/(x - 1) по всем элементам набора, не меньше единицы. Авторы проверили гипотезу для некоторых конкретных наборов, вроде того самого 3, 4, 5, но в общем виде доказать не смогли.

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

Именно в таком облегченном виде задача и попала на сайт "проблемы Эрдеша". Там она жила годами, с отсылкой к статье 1996 года, хотя формулировка фактически отличалась. Для математика, который идет от сайта к исходной работе, это не проблема: он видит исходную, более сильную гипотезу. Но для машины, которая честно берет текст с сайта и формализует именно его, разница оказывается критичной.

Aristotle устроен иначе, чем привычные языковые модели. Вместо того чтобы просто выдавать красивый текст "доказательства", он сразу генерирует строго формальный код на языке Lean, который проверяется независимым математическим ассистентом. Если Lean принимает доказательство, оно считается корректным. В случае с задачей 124 модель взяла формулировку с сайта, перевела ее в язык Lean и затем в течение нескольких часов перебирала варианты рассуждений, пока не нашла корректный формальный вывод. Проверка заняла считанные минуты.

Оказалось, что для версии задачи "с единицами" и без условия на общий делитель существует очень короткое и элементарное доказательство. Если отсортировать все степени, включая нулевые, в один список, то утверждение о том, что любое число можно представить как сумму некоторых его элементов, эквивалентно простой оценке: сумма первых n элементов списка должна быть не меньше, чем следующий элемент минус 1. Дальше используется школьная формула суммы геометрической прогрессии и условие на сумму 1/(x - 1). Оценка получается автоматически, а значит, любое натуральное число действительно можно набрать такой суммой. Доказательство занимает буквально несколько строк формальных рассуждений, но его почему-то никто не заметил почти тридцать лет.

Куратор сайта задач Эрдеша Том Блум и другие математики внимательно разобрали работу. Вывод получился осторожный. Да, Aristotle действительно нашел и формально проверил доказательство нетривиальной задачи. Да, это "настоящая" математика, а не выдавание красивого, но неподтвержденного текста. Но решена версия, которая соответствует не исходной гипотезе из статьи 1996 года, а упрощенной формулировке из обзора 1997 года и сайта. Поэтому сильная версия задачи без единиц и с дополнительным арифметическим условием по-прежнему остается открытой.

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

История с задачей 124 не первая, где крупные языковые модели и формальные доказатели вмешиваются в нарратив вокруг классических проблем Эрдеша. Несколько месяцев назад другой дуэт "человек плюс ИИ" показал, что знаменитая задача Эрдеша о Sidon-множествах, за которую когда-то назначался приз в тысячу долларов, по сути была решена еще в статье 1940-х годов, просто это так и не стало общим знанием в сообществе. Там модель помогала переводить человеческий план доказательства в язык Lean и находить технические пробелы.

В совокупности такие истории показывают реальное, а не маркетинговое место ИИ в современной математике. Модели пока не заменяют инсайт уровня Эрдеша или Грэма и не закрывают "тяжелые" гипотезы одним кликом. Но они уже умеют прочесывать огромные пространства формальных рассуждений, находить неожиданные простые аргументы для упрощенных постановок, вытаскивать забытые результаты из старой литературы и превращать человеческие идеи в строго проверяемый код. А значит, впереди нас ждет еще много случаев, когда после громкого заголовка "ИИ решил задачу" придется внимательно смотреть, какую именно формулировку он на самом деле доказал.