GPT-5.2 и ИИ Aristotle решили 50-летнюю математическую задачу Эрдёша

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 решил десять задач,