Терренс Тао: ИИ превращает математику в подобие open source-разработки

Терренс Тао, один из крупнейших математиков современности и лауреат Филдсовской премии, в интервью каналу Math Inc рассказал о трансформации математики под влиянием ИИ и формальных систем доказательств. По его словам, сочетание языков вроде Lean с нейросетями меняет саму природу математической работы — от одинокого ремесла к коллективной разработке, похожей на создание программного обеспечения.

Тао начинает с признания: около 70% работы математика — это рутина. Проверка литературы, подгонка аргументов, ручные вычисления. Раньше он пытался автоматизировать это скриптами, но технологии не позволяли. Появление ChatGPT, Copilot и языка Lean изменило ситуацию. Теперь черновую работу можно делегировать ИИ, освободив время для идей. При этом Тао подчеркивает важный нюанс: LLM сами по себе ненадежны и часто галлюцинируют, а в математике "почти верно" означает "неверно". Ценность — именно в связке: LLM выступает как креативный генератор гипотез, а на роль строго компилятора подходит Lean — язык для формальной записи и автоматической проверки доказательств.

Это не просто теория. Тао координировал проект по формализации гипотезы PFR (Polynomial Freiman-Ruzsa) на языке Lean. Обычно проверка такой работы занимает месяцы рецензирования. Они выложили задачу на GitHub, разбили на модули, а участники использовали LLM для генерации черновиков формализации — и сообщество, включая студентов и энтузиастов, собрало доказательство за три недели. Появляется то, что Тао называет "гражданской математикой": не обязательно быть профессором, чтобы закоммитить формализацию одной леммы и внести вклад в открытие.

По мнению Тао, определение математика расширится. Вместо одинокого гения у доски появятся архитекторы, которые придумывают стратегию