От олимпиад к задачам тысячелетия: хронология прорыва
Прогресс способностей LLM в математике произошел за рекордные сроки. Если в 2022 году ChatGPT ошибался даже в простых арифметических задачах, то к 2024 году reasoning-модели (OpenAI o1, DeepSeek R1) начали демонстрировать уровень золотой медали на Международной математической олимпиаде. Однако настоящий перелом наступил в 2025–2026 годах:
- Октябрь 2025: OpenAI заявила о доказательствах задач Эрдёша, но выяснилось, что модель лишь нашла известные решения (плагиат).
- Начало 2026: Появились первые новые доказательства малоизвестных задач на erdosproblems.com.
- Февраль 2026: Дональд Кнут подтвердил, что Opus 4.6 помогла ему в работе над «Искусством программирования», заставив пересмотреть взгляды на ИИ. Запущен независимый проект First Proof для академической валидации.
«Эпоха изобилия» и смена фокуса
Легендарный математик Теренс Тао охарактеризовал текущий момент как наступление «эпохи изобилия доказательств». Исторически доказательства были дефицитным ресурсом, определяющим успех ученого. Теперь, когда ИИ генерирует их массово, ценность смещается. Тао выделяет новые этапы жизненного цикла доказательства:
- Получение (ранее главный приоритет, теперь автоматизируется).
- Проверка (верификация).
- Каноникализация (интеграция в общую теорию и понимание).
Кризис доверия и роль Lean
Рост генеративных возможностей породил «золотую лихорадку» и скандалы, например, с непроверенными заявлениями об уравнениях Навье-Стокса. В ответ сообщество обратилось к формальной верификации. Ядром процесса становится язык доказательств Lean, который позволяет машинам проверять корректность рассуждений с точностью, недоступной человеческому глазу. Лейденская декларация рекомендует исследователям открыто указывать использование ИИ и нести ответственность за результаты.
Сравнение ролей: Человек vs ИИ
Несмотря на успехи, ИИ пока не обошел человека во всем. Ниже приведена сравнительная характеристика текущих возможностей:
| Критерий | ИИ (LLM/Reasoning Models) | Человек-математик |
|---|---|---|
| Генерация идей | Слабо. Использует известные паттерны, не создает новых теорий. | Сильно. Создает концептуальные прорывы и новые направления. |
| Доказательства | Сильно. Находит новые решения для узких задач, быстро проверяет гипотезы. | Слабо/Средне. Процесс медленный, но обеспечивает глубокое понимание. |
| Написание текстов | Слабо. Публикации часто хуже по качеству изложения, чем человеческие. | Сильно. Умеет структурировать аргументацию и вести научный нарратив. |
| Верификация | Сильно (в связке с Lean). Может валидировать миллионы строк кода. | Слабо. Человеческая ошибка неизбежна при больших объемах. |
Главный вопрос: зачем нужна математика?
ИИ заставил математиков задать метавопрос: какова цель фундаментальной науки, если машина может найти доказательство гипотезы Римана, но никто из людей не сможет его прочитать? Дискуссия сместилась от оценки по количеству публикаций к вопросу о понимании. Если ИИ берет на себя рутину доказательств, роль человека трансформируется в роль куратора, интерпретатора и создателя новых смыслов, а не просто «генератора PDF-файлов».
Источник: Habr ↗