В 2014 году Тао участвовал в дискуссии лауреатов Breakthrough Prize in Mathematics. Тогда он предположил, что математики будущего будут писать работы не только в LaTeX, а на языке, который программа сможет перевести в строгую формальную запись. Если в доказательстве не хватает шага, компьютер сразу выдаст ошибку. На фоне привычной математики, где статью проверяют рецензенты, такая картина выглядела почти фантастикой.

Идея особенно удивляла из-за самого Тао. Он прославился как редкий математический вундеркинд: в два года уже показывал детям постарше, как считать с помощью кубиков, в семь начал изучать матанализ, в 10 получил бронзу на Международной математической олимпиаде, затем стал самым молодым серебряным и золотым медалистом этой олимпиады. В 15 лет он окончил университет в Аделаиде, позже поступил в докторантуру Принстона, а в 2006 году получил медаль Филдса.

Но Тао всегда тянуло к совместной работе. Один из главных результатов его ранней карьеры появился вместе с Беном Грином. Они доказали, что среди простых чисел встречаются сколь угодно длинные арифметические прогрессии. Проще говоря, даже в наборе чисел, который выглядит хаотичным, можно найти длинные цепочки с одинаковым шагом.

В конце 2000-х Тао активно писал в блоге о своих исследованиях и обсуждал идеи с читателями. Примерно тогда же Тимоти Гауэрс предложил формат Polymath Project: открытую работу над математическими задачами, где любой участник мог предложить идею, уточнение или кусок доказательства. Первый проект был посвящён теореме Хейлса — Джуетта о закономерностях в раскрашенных решётках. После нескольких месяцев обсуждений группа выпустила статью под коллективным псевдонимом D.H.J. Polymath.

Polymath показал, что большая открытая группа может решать серьёзные задачи. Но у такого подхода быстро проявилась слабость. Чем больше участников, тем больше фрагментов нужно проверять. Кто-то должен читать все предложения, искать ошибки, сопоставлять куски доказательства и следить, чтобы общий ход рассуждений не развалился. В итоге ручная проверка снова становилась узким местом.

Тао всё чаще приходил к выводу, что массовой математике нужна машинная проверка. Здесь важны системы вроде Lean. Lean позволяет записывать математические утверждения и доказательства как код. Программа не оценивает красоту идеи и не заменяет математика, но строго проверяет логику: если шаг не доказан, доказательство не проходит.

Тао начал серьёзно осваивать Lean в октябре 2023 года. Для первого эксперимента он взял короткое доказательство, связанное с неравенством Маклорена. В обычной статье такой текст занимал 10 страниц. При переводе в Lean быстро выяснилось, что трудными становятся не самые глубокие места, а то, что на бумаге обычно считают очевидным. Например, человеку не нужно объяснять, что сумма трёх чисел, каждое из которых больше единицы, не меньше трёх. Lean требует сослаться на уже доказанное утверждение. Даже число 3 приходится задавать точно: натуральное, целое или вещественное.

Почти через месяц Тао всё же довёл формализацию до конца. Математический результат был скромным, а код, по его собственным оценкам, неидеальным. Но опыт оказался важнее: Тао сам увидел, как выглядит доказательство, которое проверяет не человек, а программа.

Почти сразу после этого он попробовал применить Lean к более серьёзной работе. Вместе с Беном Грином, Тимоти Гауэрсом и Фредди Мэннерсом Тао завершил доказательство по задаче из аддитивной комбинаторики. Речь шла о множествах чисел и их попарных суммах. Если взять 10 случайных чисел и сложить все разные пары, обычно получится около 50 сумм. Если взять числа от одного до 10, сумм будет всего 17, потому что многие варианты повторяются: например, 1 + 6, 2 + 5 и 3 + 4 дают один и тот же результат.

Такие множества интересны математикам, потому что малое число попарных сумм часто говорит о скрытом порядке. В данном случае работа была связана с полиномиальной гипотезой Фреймана — Ружи. Эта гипотеза описывает, насколько упорядоченными должны быть множества, у которых сумма с самим собой растёт медленно. В ноябре 2023 года авторы выложили доказательство на arXiv, а затем Тао предложил перевести его в Lean.

Соавторы не стали учить систему проверки доказательств, поэтому Тао открыл канал в чате Lean-сообщества и позвал добровольцев. В отличие от Polymath, группа не искала новое доказательство. Участники брали уже готовую статью и переводили её в строгий вид, который Lean может проверить.

Работа быстро стала коллективной. Аспирант Яэль Диллис помог разбить доказательство на 13 разделов. Тао дробил рассуждения на маленькие леммы, чтобы разные участники могли брать небольшие задачи. В обычной статье вспомогательное утверждение может занимать около 20 строк, а здесь многие куски сводили к пяти строкам. Такой формат позволял подключать людей с разным уровнем опыта.

Сначала участники формализовали базовые понятия из теории вероятностей, которых ещё не хватало в Mathlib, библиотеке формализованной математики для Lean. Среди них была энтропия Шеннона. В теории информации она измеряет неопределённость: грубо говоря, насколько трудно заранее предсказать результат случайного процесса.

К концу ноября Тао уже почти не писал код сам. Он распределял задачи, уточнял формулировки и помогал держать общий план. Один из участников закрыл предложенное задание меньше чем за час. Для Тао это стало важным подтверждением: математик может вести проект формализации, даже если не является сильным специалистом по Lean.

Вокруг проекта быстро начался спор. Одни увидели в нём начало быстрой формализации крупных результатов. Другие говорили, что добровольцы пришли прежде всего из-за имени Тао. Появился и более практичный вопрос: как учитывать такой вклад в академической карьере. Молодой математик может потратить много сил на формализацию, но университеты и грантовые комиссии пока не всегда оценивают такую работу наравне с обычными статьями.

К 2024 году Тао всё активнее продвигал связку из трёх элементов: (1) человеческой идеи, (2) ИИ-помощника и (3) строгой проверки в Lean. Он не считал, что языковые модели скоро заменят математиков. Наоборот, ранние эксперименты показали ему их слабость: модели уверенно предлагают решения, но плохо отличают хорошую мысль от неверной. На переднем крае математики, где мало готовых примеров, такой помощник легко ошибается.

Зато ИИ может быть полезен в задачах, которые делятся на тысячи небольших шагов. Человек выбирает направление и работает с трудными местами. ИИ помогает с простыми фрагментами. Lean проверяет результат и не пропускает логические дыры. Именно эту схему Тао решил проверить в проекте Equational Theories.

Поводом стал вопрос на MathOverflow о связи между алгебраическими законами. Например, сложение может подчиняться переместительному закону: x + y = y + x. Другой закон — сочетательный: (x + y) + z = x + (y + z). Один закон не обязательно следует из другого. Тао заинтересовался не отдельной задачей, а полной картой таких связей.

Если ограничиться законами, где операция применяется ровно четыре раза, получается 4694 варианта. Каждый закон может следовать или не следовать из любого другого. Всего выходит около 22 млн возможных связей. Для ручной работы это слишком много. Для проекта с добровольцами, скриптами, автоматическими доказателями теорем и Lean — подходящий масштаб.

Участники начали с магм. В алгебре магма — это множество с одной бинарной операцией. У этой операции заранее не требуют привычных свойств вроде сочетательности или переместительности. Поэтому магмы удобно использовать как первый фильтр. Если закон не работает даже на такой простой структуре, он не может служить общим следствием для более сложных случаев.

Добровольцы проверили миллионы простых вариантов с помощью Python-скриптов. Уже за два дня стало понятно, что проект движется намного быстрее ожиданий. За короткое время участники закрыли более 99% из 22 млн возможных связей. Дальше оставшиеся случаи разбирали автоматические доказатели теорем и сами математики.

Через месяц группа сократила число нерешённых вопросов до 238. К концу ноября оставалось 138, в начале нового года — около 30, а к концу марта участники застряли на четырёх последних случаях. Но полное закрытие таблицы не было главным итогом. Тао хотел проверить, можно ли вести математическое исследование как большой эксперимент: (1) построить огромную карту вариантов, (2) быстро отсечь простые случаи и (3) оставить людям самые трудные места.

Проект дал и неожиданный математический результат. Во время работы участники наткнулись на новую конструкцию, которую Тао назвал когомологией магм. Когомология — стандартный раздел современной алгебры и геометрии, где изучают скрытые препятствия и связи внутри математических структур. Вариант для магм выглядел необычно. Тао спросил математика Джона Баэза, встречалась ли такая конструкция раньше, и тот ответил, что не встречал.

Для Тао это было главным доказательством пользы нового подхода. Проект не обещал открыть большую теорему, но сам способ массового поиска вывел участников к новой идее. Значит, формальные системы и автоматические проверки могут не только подтверждать уже известные доказательства, но и помогать исследовать большие пространства вариантов.

Тао сравнивает возможную перемену с тем, что давно произошло в физике. Теоретики по-прежнему важны, но рядом с ними работают (1) большие экспериментальные группы, (2) приборы, (3): программы и (4) массивы данных. В математике похожая модель только появляется. Вместо детекторов частиц здесь используются (1) базы формализованных доказательств, (2) автоматические доказатели, (3) языковые модели и (4) команды людей, которые разбивают большую задачу на множество проверяемых шагов.

Новый подход не отменяет работу математика. Меняется распределение труда. (1) Человек выбирает вопрос, понимает смысл результата, строит стратегию и решает, какие направления развивать. (2) Компьютер проверяет логику, перебирает простые случаи и помогает держать вместе огромные проекты, где ручная проверка уже не справляется. Тао давно говорил о такой математике. Теперь он показывает, как она может выглядеть на практике.