- Связка GPT-5.2 Pro и ИИ Aristotle решила открытую 50-летнюю математическую задачу Эрдёша #728.
- Доказательство формализовано в proof assistant Lean и верифицировано машинно, признано авторитетным математиком Теренсом Тао.
- Это первый случай, когда крупная языковая модель создала оригинальное доказательство, не основанное на известных решениях.
В начале 2026 года команда, включающая передовые системы искусственного интеллекта — языковую модель GPT-5.2 Pro и специализированный математический ИИ Aristotle — успешно решила задачу Эрдёша #728, остававшуюся открытой с 1975 года. Эта проблема, сформулированная Полом Эрдёшем, Рональдом Грэхемом, Имре Рузой и Эрнстом Страусом, касалась условия делимости факториалов при определённых ограничениях на целые числа и долгое время не имела разрешения в научном сообществе.
Уникальность достижения заключается не только в нахождении решения, но и в том, что доказательство полностью формализовано в системе Lean и машинно верифицировано, что гарантирует его строгость. Признание Теренса Тао — одного из ведущих современных математиков — подчёркивает серьёзность результата. Важно отметить, что ранее попытки решения выдвигали лишь тривиальные варианты, противоречащие изначальному замыслу задачи. Новое доказательство доказало существование бесконечно множества решений при заданных параметрах, точно отражающих требования постановки.
Процесс работы был построен на тесном взаимодействии ИИ и человеческих специалистов: GPT-5.2 Thinking исследовал проблему и предлагал основные идеи, GPT-5.2 Pro исправлял неточности и переводил аргументы в формат LaTeX, а Aristotle отвечал за формализацию в proof assistant Lean. При первом подходе результат был частичным, после уточнения условий модель справилась с задачей. Хотя управлением процесса занимались два человека, основная математическая работа выполнена искусственным интеллектом.
Ранее, осенью 2025 года, заявления об успехах ИИ в решении задач Эрдёша вызвали споры — было выявлено, что GPT-5 часто находил уже известные, но «потерянные» решения. В случае задачи #728 тщательный анализ литературы не выявил предшествующих доказательств, что делает данный результат подлинным прорывом. При этом эксперты честно признают, что подобное решение могло опираться на знания, полученные из работ 2015 года, присутствующих в обучающих данных модели.
Тао подчёркивает, что полностью исключить влияние тренировочных данных невозможно, однако данное достижение оказалось в числе первых, когда ИИ предоставил решение, достойное научной публикации. Разработчик платформы erdosproblems.com отмечает, что это может стать началом масштабного использования ИИ для раскрытия нерешённых задач. Стартап Harmonic с Aristotle уже продемонстрировал высокие способности формализации и решения математических задач, а с выпуском новых поколений генеративных моделей ожидается резкий рост подобных результатов.
