Теренс Тао — лауреат медали Филдса и один из наиболее цитируемых математиков современности — изложил концепцию, которая меняет представление о том, как вообще делается математика. Его тезис: ИИ дисциплины открывает возможность для разделения труда.
В физике, химии или биологии специализация существует давно: одни исследователи ставят гипотезы, другие проводят эксперименты, третьи занимаются статистической обработкой данных. В математике такого никогда не было. Один человек должен был самостоятельно пройти весь путь: сформулировать задачу, выработать стратегию доказательства, реализовать её технически, проверить каждый шаг и оформить результат. Передать часть этой цепочки другому человеку было практически невозможно — слишком высок порог вхождения в контекст чужой работы.
ИИ и системы формальной верификации, по мнению Тао, способны закрывать именно эти «пробелы в навыках» внутри исследовательских коллабораций. Если один математик силён в постановке задач, но слаб в рутинных вычислениях, ИИ может взять на себя техническую часть. Формальная верификация — автоматическая проверка доказательств на корректность с помощью специализированных систем вроде Lean или Coq — позволяет убедиться, что результат надёжен, даже если его генерировал не человек.
ИИ может закрывать пробелы в навыках при совместной работе, но без верификации порождает лавину непроверенных идей.
Однако Тао указывает на ключевое ограничение: если ИИ генерирует стратегии без их верификации, исследователи получают лавину непроверенных идей. Это не ускоряет науку, а засоряет её. Отсюда — принцип, который Тао формулирует прямо: «Уровень автоматизации и мощности ИИ, который можно продуктивно использовать до того, как результат превратится в мусор, примерно пропорционален строгости верификации». Иными словами, чем надёжнее система проверки, тем больше можно доверить машине.
Это требование создаёт системную зависимость: новая модель математической работы функционирует только при одновременном прогрессе сразу в нескольких направлениях — генерации идей, формальной верификации и инструментах совместной работы. Если одно звено отстаёт, вся конструкция теряет смысл.
Тао описывает будущее математики как «индустриальную»: вместо одиночек, годами работающих над одной теоремой, — большие команды с ИИ-поддержкой, способные охватывать более широкое пространство задач, пусть и с меньшей глубиной на каждом направлении. При этом роль человека остаётся центральной — именно потому, что производительность ИИ неравномерна: модели блестяще справляются с одними подзадачами и беспомощны в других. Люди делают «вдохновенные догадки» на основе нескольких наблюдений там, где ИИ перебирает миллиарды точек данных.
Для отрасли в целом этот взгляд значим за пределами математики. Принцип соответствия между уровнем автоматизации и строгостью верификации применим к любой области, где качество результата критично: от разработки программного обеспечения до клинических исследований. Математика в этом смысле — предельный случай, где верификация абсолютна, а значит, именно здесь новая модель может быть реализована наиболее последовательно.
