Математика в эпоху ИИ: взгляд Теренса Тао на ICM 2026

24 июля 2026 года Теренс Тао, профессор Калифорнийского университета в Лос-Анджелесе и лауреат Филдсовской премии, прочитал доклад «Mathematics in the age of AI» на ICM 2026 в Филадельфии (Pennsylvania Convention Center). Слайды, опубликованные на его официальном сайте, напоминают исторический контекст «кризиса оснований» (1900‑1930) и предлагают новый кризис — на этот раз не вокруг аксиом, а вокруг ценностей и практик математического сообщества. Тао формулирует «Community Response Question», которая не является традиционным математическим вопросом: это вопрос метаматематический, политический, этический и культурный. При этом он отделяет «AI Capability Conjecture» (насколько инструменты действительно способны) от вопроса о целях и ценностях дисциплины.

Тао отмечает, что многочисленные данные, приводимые за и против разных версий гипотезы, собраны не в контролируемых научных условиях, а публичные свидетельства несут на себе отпечаток отбора, ненаучных стимулов и незаявленных издержек. Единственное исключение, которое он называет, — независимый проект First Proof (1stproof.org): его вторая партия из десяти задач была протестирована в контролируемых условиях 28 мая 2026 года на четырёх ИИ-«харнессах», семь задач из десяти были решены на уровне публикации по меньшей мере одной командой, а корректность и изложение оценивали эксперты. Результаты задокументированы в препринте arXiv 2606.18119 и на странице Center of Mathematical Sciences and Applications Гарварда. Это по-прежнему выборка из десяти задач, которую нельзя распространить на всю математическую науку; не проверено и то, каким коммерческим системам соответствуют четыре протестированных харнесса.

Смысловой центр доклада — разложение математического производства на пять стадий: порождение, проверка, изложение, публикация и канонизация. По словам Тао, ИИ и ассистенты автоформализации (Rocq, HOL, Lean) уже ускорили первые две стадии, тогда как последние три по-прежнему держатся на человеческой работе. Тао упоминает и ИИ-доказательства на erdosproblems.com, где решения не проверяются людьми-рецензентами, — конкретный симптом проблемы надёжности. Он критикует также автоматическое изложение: «естественное трение», то есть трудности, с которыми сталкивается человек-автор, даёт читателю полезные сигналы, а слишком гладко отполированное ИИ доказательство способно эти подсказки стереть. Как формулирует сам Тао, «In short, we will transition from an era of proof scarcity to an era of proof abundance».

Тао ссылается на Leiden Declaration on Artificial Intelligence and Mathematics (2 июня 2026) и предлагает практическое правило: если авторы не в состоянии убедительно прочитать ясный доклад экспертного уровня о собственных результатах — корректный и с правильными ссылками, — то результат публиковать не следует. Он заключает, что анализ решения задач должен распространяться на преподавание, наставничество, наём и финансирование, а использование ИИ в обучении следует строго ограничить. Финальное замечание: публичный документ выступления — это слайды; официальной расшифровки устного доклада не существует.