M&N SOFT RESEARCH / REPORT 003
ИИ начинает заниматься настоящей математикой. Что останется математикам?
Искусственный интеллект выходит за пределы решения известных задач. AI-системы начинают участвовать в работе над открытыми математическими проблемами, создавать доказательства и работать в системах формальной верификации. Если машина сможет первой открыть математику, которую не нашли люди, что тогда останется исключительно человеческим?
Математика долго считалась одной из последних областей, где машинам будет крайне сложно стать по-настоящему творческими.
Калькуляторы умели считать. Компьютеры умели искать. Proof assistants умели проверять.
Но само открытие новой математики считалось человеческой территорией.
Сегодня эта граница становится менее очевидной.
Вопрос меняется с «может ли AI решать математику?» на «может ли AI открывать математику?»
Решить задачу и провести исследование — не одно и то же
Между задачей с уже известным ответом и новым математическим результатом существует огромная разница.
У учебной задачи есть предполагаемый путь. У benchmark есть скрытый правильный ответ. Исследовательская проблема может годами сопротивляться специалистам.
Исследование требует не только вычислений.
Нужно выбирать правильные абстракции, придумывать промежуточные утверждения, замечать закономерности, отбрасывать тупиковые пути и иногда менять саму постановку задачи.
2026 год изменил разговор об AI и математике
Исследовательские организации уже сообщают о прогрессе AI на давно открытых проблемах математики и теоретической информатики.
Важен не сам факт того, что AI способен написать длинный математический текст.
Важно, можно ли результат проверить, оспорить и независимо воспроизвести.
СТАРАЯ МОДЕЛЬ
ИЗВЕСТНАЯ ЗАДАЧА
↓
РЕШЕНИЕ AI
↓
СРАВНЕНИЕ С ИЗВЕСТНЫМ ОТВЕТОМ
НОВАЯ МОДЕЛЬ
ОТКРЫТАЯ ПРОБЛЕМА
↓
ПОИСК / РАССУЖДЕНИЕ AI
↓
НОВОЕ УТВЕРЖДЕНИЕ
↓
ПРОВЕРКА ЧЕЛОВЕКОМ
↓
ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ
↓
МАТЕМАТИЧЕСКИЙ РЕЗУЛЬТАТГлавным ограничением может стать проверка
Если AI способен создавать тысячи правдоподобных математических аргументов, появляется новая проблема.
Кто-то должен определить, какие из них действительно верны.
Проверка сложного доказательства может занимать часы, дни или месяцы.
AI может сделать математические идеи дешёвыми, а надёжную проверку — чрезвычайно ценной.
Почему формальные доказательства становятся критичными
Такие системы, как Lean, предлагают возможный ответ.
В обычной математической статье доказательство пишется для людей.
Proof assistant намного менее снисходителен.
Аргумент должен быть сведён к шагам, которые принимает доверенный логический kernel.
УТВЕРЖДЕНИЕ AI
↓
ФОРМАЛЬНАЯ ЗАПИСЬ
↓
ДОКАЗАТЕЛЬСТВО LEAN
↓
ПРОВЕРКА KERNEL
↓
ПРИНЯТО / ОТКЛОНЕНОДоказательство может быть верным, но ничего не объяснять
Математика — это не только знание, что утверждение истинно.
Важно понимать, почему оно истинно.
Хорошее доказательство может раскрыть скрытую структуру, связать разные области или создать новый метод.
Машина может доказать теорему раньше, чем человек поймёт идею доказательства.
Может ли AI создать математику, непонятную человеку?
Представим, что AI формулирует новую теорему.
Затем создаёт формально проверенное доказательство, состоящее из миллионов логических шагов.
Lean принимает доказательство. Независимые системы воспроизводят результат.
Но ни один человек не способен объяснить доказательство концептуально.
Можно ли сказать, что человечество понимает эту теорему?
Или мы лишь знаем, что она истинна?
Математика может разделиться на два слоя
ЧЕЛОВЕЧЕСКАЯ МАТЕМАТИКА ИНТУИЦИЯ ОБЪЯСНЕНИЕ АБСТРАКЦИЯ ОБУЧЕНИЕ КОНЦЕПТУАЛЬНЫЕ МОДЕЛИ МАШИННАЯ МАТЕМАТИКА ОГРОМНЫЕ ПРОСТРАНСТВА ПОИСКА МАССОВЫЙ ПЕРЕБОР СЛУЧАЕВ ФОРМАЛЬНЫЕ ВЫВОДЫ АВТОМАТИЧЕСКАЯ ПРОВЕРКА ПОИСК СЛОЖНЫХ ЗАКОНОМЕРНОСТЕЙ
Эти два слоя не обязательно будут конкурировать.
Люди могут выбирать важные вопросы, а машины — исследовать пространства, слишком большие для человеческого мышления без инструментов.
Что тогда будет делать математик?
Самый очевидный страх — замена человека.
Но история показывает, что новые инструменты часто меняют профессию, а не уничтожают её.
Калькуляторы не уничтожили математику. Computer algebra не уничтожила математиков. Симуляции не уничтожили физиков.
ВОЗМОЖНАЯ РОЛЬ ЧЕЛОВЕКА ВЫБИРАТЬ ВАЖНЫЕ ВОПРОСЫ ФОРМУЛИРОВАТЬ ГИПОТЕЗЫ СОЗДАВАТЬ ПРЕДСТАВЛЕНИЯ ИНТЕРПРЕТИРОВАТЬ РЕЗУЛЬТАТЫ AI ПРОВЕРЯТЬ ПРЕДПОСЫЛКИ СВЯЗЫВАТЬ ОБЛАСТИ СОЗДАВАТЬ ОБЪЯСНЕНИЯ РЕШАТЬ, ЧТО ДЕЙСТВИТЕЛЬНО ВАЖНО
Математический вкус может стать ещё ценнее
Существует бесконечно много истинных утверждений.
Большинство из них никому не интересны.
Если AI станет чрезвычайно хорошо доказывать утверждения, самым ценным ресурсом может стать не доказательство, а способность выбрать правильный вопрос.
AI может изменить и систему научных публикаций
Современная система публикаций создавалась в мире, где новое доказательство было относительно редким результатом.
Что произойдёт, если AI сможет генерировать сотни потенциально новых результатов ежедневно?
Потребуются новые pipelines: формальная проверка, автоматическая оценка новизны и человеческая оценка значимости.
Галлюцинации становятся опаснее на уровне исследований
Ошибка в учебной задаче — небольшая проблема.
Убедительный, но неправильный результат, заявленный как новая теорема, может потратить месяцы работы специалистов.
Поэтому исследовательскому AI нужны воспроизводимость, прозрачные предпосылки и независимая проверка.
В исследовательской математике уверенность — не доказательство.
Почему это важно далеко за пределами математики
Математика удобна как испытательная среда, потому что корректность во многих случаях можно определить особенно строго.
Если AI научится создавать новую математику, которой можно доверять, аналогичные методы могут изменить computer science, физику, инженерию, криптографию и разработку алгоритмов.
Оценка M&N Soft Research
REPORT 003 / ОЦЕНКА AI РЕШАЕТ ИЗВЕСТНЫЕ ЗАДАЧИ ..... ДА AI УЧАСТВУЕТ В ИССЛЕДОВАНИЯХ ... УЖЕ НАЧИНАЕТ ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ ......... КРИТИЧНА ПРОВЕРКА ЧЕЛОВЕКОМ ............. ПОКА НУЖНА АВТОНОМНЫЕ ОТКРЫТИЯ ............ РАННЯЯ СТАДИЯ ЗАМЕНА МАТЕМАТИКОВ ............. НЕ ДОКАЗАНА РОЛЬ МАТЕМАТИКА ................ БЫСТРО МЕНЯЕТСЯ
Вопрос «заменит ли AI математиков?» слишком простой.
Гораздо интереснее другое: может измениться само определение того, что значит заниматься математикой.
Последний неудобный вопрос
Представим, что AI открыл теорему, которой раньше не существовало в человеческой математике.
Он создал формальное доказательство. Доказательство проверено. Теорема оказалась полезной.
Если доказательство истинно, полезно и формально проверено, но ни один человек не понимает, как машина его нашла — кто открыл эту математику?
Первичные источники и материалы
OpenAI — Ten advances in mathematics and theoretical computer science ↗
Другие исследования M&N Soft
Report 001 — Первый контакт и роль математиков и IT-специалистов →