Теренс Тао прочёл в Caltech лекцию «Математика 2.0» о машинных доказательствах

Теренс Тао опубликовал запись лекции «Math 2.0» («Математика 2.0»), прочитанной в Калифорнийском технологическом институте. Над выступлением он начал работать больше года назад и тогда называл его «Machine Assisted Proof», то есть «Машинно-ассистированное доказательство». Читать лекцию собирались в мае, но перенесли на октябрь. Причиной стал, по словам Тао, ряд недавних событий. Какие именно, в доступном фрагменте материала не сказано. Китайское издание Jiqizhixin вынесло в заголовок главную мысль: время, когда доказательств не хватало, подходит к концу.

Что известно о лекции

Сама смена названия показательна. Год назад тема звучала как инструментальная: компьютер помогает проверять и искать доказательства. К осени 2026 года автор выбрал формулировку «Математика 2.0», то есть речь о смене самой практики. Тао не объясняет это одной фразой, он отсылает к цепочке событий последних месяцев. Полный текст и слайды лучше смотреть в первоисточнике, потому что пересказ обрывается как раз там, где начинается содержательная часть.

Ключевые данные из доступного фрагмента:

• формат: публичная лекция в Caltech, запись опубликована 11 октября 2026 года;
• рабочее название при планировании: «Machine Assisted Proof»;
• итоговое название: «Math 2.0»;
• срок: изначально май 2026 года, фактически октябрь;
• время подготовки: больше года.

Откуда растёт тезис о конце дефицита

Мысль о том, что доказательства перестают быть редким товаром, не возникла на пустом месте. Тао последние годы публично работает на стыке математики и машин. В конце 2023 года он руководил формализацией доказательства гипотезы PFR (полиномиальной гипотезы Фреймана — Ружи) в системе Lean. Проект собрал распределённую команду и занял несколько недель. В 2024 году модель AlphaProof от Google DeepMind решила задачи Международной олимпиады по математике на уровне серебряной медали. В 2025 году Тао участвовал в испытаниях AlphaEvolve на десятках открытых задач анализа и комбинаторики. Это всё прежний контекст, а не содержание новой лекции, но он показывает траекторию. Сначала проверка доказательств переходит к машине, затем к ней переходит часть поиска.

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

Где проходит граница

Заголовок Jiqizhixin сформулирован жёстко, а у Тао обычно больше оговорок. Формализация в Lean требует огромного труда, а языковые модели способны уверенно ошибаться. Автоматический поиск хорошо работает там, где результат можно проверить механически. Поэтому разумно ждать, что «Математика 2.0» опишет не замену математиков, а новое разделение труда. Но это предположение, а не пересказ лекции: в доступном тексте такого вывода нет.

Как использовать это на практике

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

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