Теренс Тао получил Филдсовскую медаль в 2006 году во многом благодаря совместной работе с Беном Грином — они доказали, что в простых числах неизбежно встречаются арифметические прогрессии. Тао всегда любил коллаборации, считал их главным способом открывать новые идеи. В 2009 году он подключился к Polymath Project Тимоти Гауэрса — попытке решать сложные математические задачи силами десятков участников в комментариях к блогу. Первый проект с псевдонимным авторством «D.H.J. Polymath» удался, но Тао быстро понял ограничения: модерировать поток добровольцев и вручную проверять их работу было узким местом. Нужна была компьютерная верификация.
Тао знал о формальной математике, но считал её непрактичной. Летом 2022 года он организовал воркшоп, а Кевин Баззард уговорил его попробовать Lean — систему, где доказательства пишут и проверяют как код. В октябре 2023 года Тао начал осваивать Lean4. Первая попытка формализовать короткую теорему заняла почти месяц — простые вещи вроде «сумма трёх чисел больше 1 равна хотя бы 3» требовали поиска готовой леммы в Mathlib. Но Тао стал частью сообщества.
Параллельно Тао с Беном Грином, Тимоти Гауэрсом и Фредди Мэннерсом решали гипотезу Полиномиального Фреймана-Ружи (PFR) о суммсетах — коллекциях чисел, полученных сложением всех уникальных пар. К ноябрю 2023 года доказательство было готово. Тао предложил формализовать его в Lean. Соавторы не захотели тратить время, но Тао запустил проект в чате Lean-сообщества и набрал добровольцев. Доказательство разбили на 13 секций и сотни коротких лемм по пять строк — это позволяло делать маленькие вклады. К концу ноября Тао почти не писал код сам, только координировал. Проект завершился быстро, но возникла дискуссия: работает ли метод для обычных математиков, а не для «звёзд» вроде Тао. Йохан Коммелин из Mathlib заметил, что вклад в формализацию пока не ценится при приёме на работу.
В 2024 году Тао стал публичным пропагандистом машинной математики. Он считал, что AI (LLM) хороши для простых задач, но на переднем крае науки беспомощны. Решение — гибрид: люди дробят проблему на тысячи мелких кусков, AI решает лёгкие, а результаты проверяет Lean. Для демонстрации он запустил проект Equational Theories — нужно было проверить 22 миллиона логических связей между 4 694 алгебраическими законами (операции с четырьмя применениями). За два дня Python-скрипты на простейших структурах (магмах) решили 99% задач. Затем подключились автоматические доказатели и люди. Через месяц осталось 238 неподтверждённых импликаций, к марту 2024 — всего четыре. Проект не просто дал карту зависимостей, а породил новую математическую конструкцию — «магма-когомологии», которую не видел даже эксперт Джон Базз. Тао утверждает: математика может стать экспериментальной, как физика с её коллаборациями вроде CERN. И он не собирается возвращаться к старому.