Знаменитый математик Теренс Тао представил видение трансформации математической дисциплины под влиянием ИИ. В своем докладе он анализирует, как автоматизированные системы меняют процесс доказательства теорем, поиска закономерностей и верификации данных. По мнению ученого, ИИ становится полноценным «соавтором», который берет на себя рутинные вычисления и поиск формальных ошибок, позволяя математикам сосредоточиться на концептуальном творчестве и постановке задач.
Тао подчеркивает, что интеграция нейросетей в научный процесс требует изменения подходов к обучению и академической работе. Математики будущего должны будут не только владеть классическим аппаратом, но и эффективно взаимодействовать с формальными системами верификации, такими как Lean. Это позволит сократить время от гипотезы до строгого доказательства, которое раньше занимало годы работы целых исследовательских групп.
Основной акцент делается на симбиозе человеческой интуиции и вычислительной мощности ИИ. В то время как модели пока склонны к «галлюцинациям» в сложных логических цепочках, их способность перебирать огромные пространства вариантов делает их незаменимыми в экспериментальной математике. Это меняет саму природу публикации научных работ, где верифицируемый код становится таким же важным элементом, как и текстовое описание.
Ключевые факты
- Теренс Тао рассматривает ИИ как инструмент для автоматизации формальной верификации математических доказательств.
- Использование систем типа Lean становится критически важным навыком для современной математики.
- ИИ-модели позволяют значительно ускорить процесс поиска контрпримеров и проверки гипотез в теории чисел и комбинаторике.
- Основная роль математика смещается от ручного вывода формул к управлению и проверке результатов, сгенерированных алгоритмами.
- Доклад подготовлен в рамках подготовки к Международному конгрессу математиков (ICM) 2026 года.