ИИ решил задачу Эрдёша: прорыв в математике!

6 января 2026 года связка GPT-5.2 Pro и математического ИИ Aristotle от стартапа Harmonic решила задачу Эрдёша #728 — открытую проблему о делимости факториалов, поставленную в 1975 году Полом Эрдёшем, Рональдом Грэхемом, Имре Рузой и Эрнстом Страусом. Доказательство формализовано в proof assistant Lean и верифицировано машинно. Задача признана решенной Теренсом Тао, — одним из самых уважаемых математиков современности. Это первый случай, когда LLM сгенерировала по-настоящему новое доказательство открытой математической задачи Эрдёша, а не переоткрыла уже существующее в литературе.

Задача #728 спрашивает: существует ли бесконечно много целых чисел a, b, n при определенных ограничениях, таких что a!b! делит n!(a+b−n)! и при этом a+b > n + C·log(n)? Формулировка оказалась неоднозначной — команда AlphaProof от DeepMind ранее нашла тривиальные решения, не соответствующие духу задачи. Авторы нового доказательства — студент-математик под ником AcerFur (KStarGamer_) и пользователь Reddit ThunderBeanage — показали, что для любых констант 0 < C₁ < C₂ существует бесконечно много решений с b = n/2, a = n/2 + O(log n), что соответствует изначальному замыслу авторов задачи.

Процесс был организован следующим образом: сначала GPT-5.2 Thinking исследовал задачу и предложил подход к доказательству, затем GPT-5.2 Pro исправил мелкие ошибки и перевел аргумент в LaTeX, после чего Aristotle формализовал доказательство в Lean. Когда первая версия дала лишь частичный результат, команда вернулась к GPT-5.2 с уточненными ограничениями — и модель справилась. Весь процесс координировали два человека, но математическую работу выполнял ИИ.

Осенью 2025 года вокруг AI и задач Эрдёша было много шума: в октябре OpenAI заявила, что GPT-5 решил десять задач, но при проверке оказалось, что ИИ просто нашел для открытых задач человеческие решения, затерявшиеся в литературе — кстати, возможность ИИ каталогизировать потерянные решения сама по себе важна для науки. Но задача #728 стала первым случаем, когда тщательная проверка литературы не выявила предшественников.

Авторы и рецензенты честно указывают на оговорки: решение, вероятно, вдохновлено работой Карла Померанса 2015 года, которая могла быть в обучающих данных GPT-5.2. Сам Тао отмечает, что невозможно доказать отсутствие влияния тренировочных данных. Кроме того, задача #728 относится к категории "низковисящих фруктов" — менее исследованных проблем из хвоста коллекции Эрдёша, которые не считаются сложными для решения, но до которых просто не добрались серьезные математики. Тем не менее Tfbloom, автор сайта erdosproblems.com, написал: "Это первый случай, когда AI сгенерировал доказательство, с которым аспирант мог бы прийти ко мне, и я бы сказал — это стоит опубликовать".

На wiki-странице Тао сейчас зафиксировано несколько десятков примеров AI-вкладов в задачи Эрдёша разной степени значимости: от решений с большим участием ИИ до неудачных попыток. Aristotle от Harmonic (стартап с оценкой $1.45 млрд) уже формализовал десятки доказательств и показал уровень золотой медали на Международной математической олимпиаде 2025. Математики ожидают, что со следующим поколением моделей — GPT-5.5 или Gemini 3.5 — поток решений увеличится.

В общем, пока люди спорят о смысле жизни, искусственный интеллект спокойно решает математические задачи. Видимо, у него просто больше свободного времени.