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