ИИ-модели начали решать сложные математические задачи

[душман]

В минувшие выходные инженер-программист Нил Сомани тестировал математические способности новой модели искусственного интеллекта OpenAI и сделал неожиданное открытие. Он поставил ChatGPT сложнейшую математическую задачу, дал чат-боту подумать 15 минут и получил готовое решение.

Исследователь оценил доказательство, провёл его формализацию при помощи средства от Harmonic, и всё оказалось в порядке. Ещё больше его впечатлила цепочка рассуждений ChatGPT — в ней ИИ воспроизвёл формулу Лежандра, постулат Бертрана и теорему о звезде Давида; а также нашёл на Math Overflow сообщение от 2013 года, где приводилось решение аналогичной задачи. 

Окончательный вариант от ChatGPT имел существенные отличия от образца и давал полное решение версии одной из задач, поставленных легендарным математиком Палом Эрдёшем — его коллекция нерешённых задач сейчас превратилась в полигон для ИИ. Этот удивительный результат не уникален — модели ИИ теперь повсеместно применяются в математике.

Средства «глубокого исследования» OpenAI отвечают за обзор литературы, а Harmonic Aristotle производит формализацию доказательств. Модель OpenAI GPT-5.2, по словам Нила Сомани, оказалась искуснее в рассуждениях, чем предыдущие версии — они уже научились решать остававшиеся открытыми задачи, по сути, расширяя границы человеческих знаний.

Пал Эрдёш оставил после себя более тысячи гипотез, которые зафиксированы сообществом математиков в сети — и они обнаружили, что GPT-5.2 на удивление хорошо справляется со сложнейшими математическими задачами. В период с 25 декабря 2025 года и по настоящий момент решены 15 задач Эрдёша, и в работе над 11 из них участвовал ИИ. 

Авторитетный математик Теренс Тао привёл восемь задач Эрдёша, в которых ИИ добился значительного прогресса; ещё в шести случаях его удалось достичь за счёт поиска и дальнейшего развития ранних исследований. Совсем без участия человека ИИ с ними пока не справился бы, но его роль становится более важной. 

«Таким образом, многие из этих более простых задач Эрдёша теперь с большей вероятностью могут решаться исключительно основанными на ИИ методами, чем человеческими или гибридными средствами», — делает вывод Теренс Тао. Ещё один важный фактор — сдвиг в сторону формализации. Это трудоёмкая задача, которая упрощает проверку и расширение математических рассуждений.

Она не требует ни ИИ, ни даже просто компьютеров, но сейчас появились средства, которые в значительной мере упростили этот процесс. Популярным, например, стал инструмент Lean, разработанный Microsoft Research ещё в 2013 году; средство Harmonic Aristotle позволяет в значительной мере автоматизировать эту задачу. Внезапный скачок в числе решённых задач Эрдёша привёл к тому, что упоминание сервисов Aristotle или ChatGPT добавляет материалам вескости в профессиональном сообществе.