Конец математики, какой мы её знали. Теренс Тао объявил новую эпоху «Математика 2.0» в науке: поиск доказательств перестанет быть главной интеллектуальной задачей человека
Искусственный интеллект научился решать математические задачи быстрее, чем научное сообщество успевает проверять результаты. На фоне публикации сотен машинных доказательств один из самых известных математиков мира, лауреат Филдсовской премии Теренс Тао, выступил в Калифорнийском технологическом институте (Caltech) с концепцией «Математика 2.0». На лекции 9 октября учёный предупредил, что прежняя система математических исследований перестаёт соответствовать возможностям ИИ, а погоня за новыми доказательствами способна даже навредить развитию науки.
Поводом для обострения дискуссии стала масштабная публикация OpenAI. Компания 6 октября открыла доступ к 722 математическим рукописям, объединённым в 372 группы взаимосвязанных результатов. Материалы подготовила экспериментальная модель, которую пока не выпустили для широкой публики. Разработчики утверждают, что ИИ решил или существенно продвинул решение сотен открытых задач из различных разделов математики. Однако публикация доказательства ещё не означает, что научное сообщество подтвердило его правильность, оригинальность и значимость.
Объём работ оказался настолько большим, что математики начали обсуждать не только достижения нейросети, но и последствия массовой публикации результатов без привычной научной экспертизы. Часть доказательств представлена в формате, который позволяет проверить логические рассуждения с помощью системы Lean, однако автоматическую проверку прошли далеко не все материалы. Даже формально правильное доказательство может повторять ранее опубликованную работу, не объяснять происхождение идеи или не давать исследователям нового понимания предмета.
Особенно резко отреагировала Association for Human Mathematics, выступающая за сохранение человеческой роли в математических исследованиях. Организация раскритиковала массовую публикацию машинных результатов, указав на проблемы авторства, возможного заимствования чужих идей и перегрузки научного сообщества. Претензии касаются не самого факта применения ИИ, а практики, при которой компании выпускают сотни решений, оставляя независимым специалистам трудоёмкую проверку. Молодые исследователи рискуют потратить месяцы на изучение материалов, которые могут обесценить уже начатые научные проекты.
Теренс Тао в своём докладе объяснил происходящее переходом от дефицита математических доказательств к их изобилию. На протяжении почти столетия поиск нового доказательства требовал исключительных интеллектуальных усилий, поэтому научные институты, система признания заслуг и исследовательские приоритеты строились вокруг редкости подобных достижений. Теперь мощные ИИ-модели способны сравнительно быстро находить решения задач, которые прежде считались сложными, причём пользователю не всегда требуются глубокие знания соответствующей области.
Математика оказалась особенно удобной дисциплиной для машинного поиска. В отличие от биологии или экспериментальной физики, многие математические результаты можно проверить без лабораторий, физических измерений и дорогостоящего оборудования. Доказательства существуют в цифровой форме, огромные массивы научной литературы доступны для обработки, а формальные системы позволяют автоматически устанавливать логическую корректность рассуждений. Сочетание подобных условий сделало математику одним из приоритетных направлений развития передовых ИИ-моделей.
При этом Тао предостерёг от преувеличения возможностей нейросетей. По словам математика, большинство задач на переднем крае современной науки остаются нерешёнными даже при огромных вычислительных затратах. Возможности ИИ крайне неравномерны. Машина способна продемонстрировать выдающийся результат в одной области и оказаться беспомощной в другой, особенно когда требуется субъективная оценка, взаимодействие с реальным миром или работа с недостаточно изученными данными. Впечатление, будто нейросети уже покорили всю математику, во многом создают сообщения об успехах, за которыми остаются невидимыми многочисленные неудачные попытки.
Главную проблему Тао видит глубже, чем профессиональная конкуренция человека с машиной. Математики занимаются исследованиями не исключительно ради окончательного ответа. Попытки решить сложную задачу часто приводят к открытию новых методов, неожиданных закономерностей и целых научных направлений. Тао сравнил открытые математические проблемы с маяками, которые помогают исследователям ориентироваться в неизвестной области. Если ИИ мгновенно доставляет готовый результат, учёные могут пропустить открытия, которые появились бы во время самостоятельного поиска. Массовое производство доказательств способно ускорить решение отдельных задач, одновременно обедняя окружающую научную среду.
Чтобы показать, почему правильный ответ не всегда равнозначен хорошему результату, математик предложил мысленный эксперимент с лекарством от рака. Представим, что продвинутая нейросеть разработала смесь ранее неизвестных химических веществ, способную уничтожать опухолевые клетки. Математическая модель предсказывает эффективность препарата, расчёты проходят формальную проверку, а сама смесь успешно завершает третью фазу клинических испытаний. Однако никто из людей не понимает, каким образом ИИ нашёл формулу и почему препарат работает.
Тао предложил задуматься, достаточно ли успешных испытаний для доверия подобному лечению. Неизвестный механизм действия может скрывать долгосрочные побочные эффекты, а ИИ теоретически способен найти решение, которое формально удовлетворяет условиям испытания, но не соответствует более широкой цели безопасного лечения. Математик спрашивает, захотел бы пациент перед введением препарата убедиться, что хотя бы один специалист понимает механизм его действия или математическую модель, использованную при разработке. Пример не описывает реальное лекарство или медицинское открытие, а показывает разницу между формально подтверждённым результатом и пониманием его последствий.
Именно человеческое понимание Тао предлагает поставить в центр «Математики 2.0». Вместо бесконечной гонки за количеством решённых задач ИИ следует использовать для объяснения уже известных теорем, поиска более понятных доказательств, объединения разрозненных исследований и обнаружения новых общих принципов. Нейросети также могут помогать строить крупные формальные библиотеки математических знаний и проверять, какие предположения действительно необходимы для доказательства конкретного результата.
Первые примеры нового подхода уже существуют. В проекте Equational Theories Project исследователи объединили человеческие и автоматизированные методы, чтобы установить истинность или ложность более 22 миллионов утверждений универсальной алгебры. Вместо последовательного изучения отдельных примеров специалисты получили возможность анализировать огромные семейства математических объектов и выявлять закономерности, которые прежде оставались недоступными. Тао рассматривает подобные исследования как переход от изучения единичных случаев к масштабным экспериментам над целыми массивами математических данных.
Другой пример связан с обновлённым Mathathon, который Caltech планирует провести 13–15 ноября. Участники будут применять открытые ИИ-инструменты не для рекордного количества новых решений, а для поиска более ясных и удобных доказательств известных результатов. Организаторы хотят сохранить за человеком понимание математических идей и требуют раскрывать, каким образом участники применяли языковые модели. Параллельно Caltech и Американский институт математики разрабатывают платформу, которая должна учитывать потребности самих исследователей, а не исключительно показатели производительности ИИ.
Спор вокруг машинных доказательств возник не на пустом месте. Ещё в сентябре OpenAI объявила о серьёзном прогрессе в задаче Навье-Стокса, относящейся к знаменитым проблемам тысячелетия. После подобных заявлений ведущие математики начали требовать прозрачных методов проверки, корректного указания авторства и соблюдения научных процедур. Компания сформировала независимую консультативную группу по математике и ИИ, однако публикация сотен новых рукописей показала, что участники дискуссии пока не договорились о приемлемых правилах работы.
Концепция Тао предлагает другой критерий успеха. Если раньше выдающимся достижением считалось получение доказательства, в эпоху мощных нейросетей всё большее значение приобретает способность объяснить результат, связать его с другими знаниями и применить без непредвиденных последствий. Человеческая роль не обязательно исчезает вместе с автоматизацией поиска, но привычные представления о научной ценности придётся пересмотреть. По мнению Тао, будущее математики зависит не от количества задач, которые ИИ сумеет закрыть, а от того, насколько глубже люди смогут понять мир с помощью новых инструментов.
suare 13 Октября Терри Тао показывает, как наука о числах будет выглядеть дальше.
Терри Тао много лет говорил о математике, где большие задачи решают не одинокие авторы и не маленькие группы, а десятки или сотни участников вместе с компьютерами. Долгое время такая идея звучала странно даже для его коллег. Сейчас один из самых известных математиков мира показывает, как этот подход может работать: люди разбивают доказательство на маленькие части, программы проверяют каждый шаг, а ИИ помогает там, где задачу можно свести к большому числу понятных фрагментов.
В 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) Компьютер проверяет логику, перебирает простые случаи и помогает держать вместе огромные проекты, где ручная проверка уже не справляется. Тао давно говорил о такой математике. Теперь он показывает, как она может выглядеть на практике.
suare 13 Октября
В заголовке чушь собачья, противоречащая логике!
Так можно придти к объявлению математики лженаукой и начать сжигать на костре.
Математика — это наука, требующая строгих, однозначных и подлежащих проверке доказательств.
При этом новые подходы возможны. При ясности и математической строгости.
Отказ от поиска и проведения надлежащих математических доказательств ввергнет в пучину хаоса.
Нельзя слепо доверять галлюционирующим ИИ.
А Тао, возможно, просто «поддался моде» производителей ИИ.
О! Собрание неолуддитов! )))
