- Терренс Тао отмечает трансформацию математики под влиянием искусственного интеллекта и формальных систем доказательств.
- Использование языков вроде Lean вместе с нейросетями меняет математику из индивидуального ремесла в коллективный и модульный процесс.
- Примером стало быстрое формализованное доказательство гипотезы Polynomial Freiman-Ruzsa с помощью ИИ и сообщества на GitHub.
Терренс Тао, один из ведущих современных математиков и обладатель Филдсовской премии, в интервью каналу Math Inc рассказал о новой эпохе в математике, вызванной развитием искусственного интеллекта и систем формальной верификации. Он отметил, что значительная часть работы математика — около 70% — связана с рутиной: поиском и проверкой информации, корректировкой аргументов и громоздкими вычислениями. Ранее такие задачи приходилось решать вручную или с помощью ограниченных скриптов, что существенно тормозило процесс.
С появлением современных технологий, таких как ChatGPT, Copilot и языка Lean для формальной записи и проверки доказательств, ситуация коренным образом меняется. Теперь рутинная часть может быть делегирована ИИ, что освобождает время учёных для реальных творческих задач. Однако Терренс Тао подчёркивает, что большие языковые модели (LLM) остаются ненадёжными и подвержены ошибкам — в математике нет места «почти верно». Именно поэтому важна гибридная модель: LLM выступают генераторами идей и гипотез, а Lean обеспечивает строгую формальную проверку и гарантии.
Тао также приводит конкретный пример успешного сотрудничества человека и ИИ в математике — проект по формализации гипотезы Polynomial Freiman-Ruzsa. Обычно верификация таких доказательств занимает месяцы из-за необходимости тщательных рецензий. В данном случае задача была разбита на модули и выложена на GitHub, где участники — от профессионалов до студентов и энтузиастов — использовали ИИ для подготовки формализаций. За три недели коллектив продемонстрировал полное доказательство, что иллюстрирует зарождение так называемой «гражданской математики», в которой вклад может делать широкий круг людей независимо от академического статуса.
По мнению Терренса Тао, роль математика в будущем будет пересмотрена. Вместо одиночных гениев появится разнообразие специалистов: архитекторы, формализаторы и «хранители» знаний, которые будут поддерживать и развивать живую, постоянно обновляющуюся базу теорем и констант. Он мечтает о системе, где улучшение одного параметра будет автоматически транслироваться на все связанные доказательства, создавая динамичную и эффективную среду научного познания. В итоге ИИ не заменит математиков, а преобразует их в создателей и управляющих сложными интеллектуальными системами.
