Ветераны Lean: спешка с математическими библиотеками, написанными ИИ, хуже их отсутствия

Контроль качества против объёма

Пост проекта Xena, авторы которого Avigad, Buzzard, Commelin и другие, оптимистичен насчёт ИИ-формализации, но тревожится за поспешные крупномасштабные проекты. Его главная мысль: «Плохая формализация существующих результатов хуже, чем её полное отсутствие.» Формализация полезна, только если ею пользуются, пишут авторы, и по их мнению, сгенерированная Claude формализация Великой теоремы Ферма (13 миллионов строк) и попытка Math, Inc. с задачей об упаковке сфер дали мало долгосрочной пользы. Формализация OpenAI уравнений Навье — Стокса на Lean дала сильный сигнал корректности, но трудночитаемое неформальное доказательство и свалку кода с откатами и несоответствиями. В качестве положительных примеров авторы приводят работу OpenAI над задачей о единичных расстояниях и работу Anthropic о плотности нулей дзета-функции.

Существующая экосистема: Mathlib (65 рецензентов, 950 участников, премия Жан-Пьера Демайи за 2026 год), Formal Conjectures, Annals Challenge, Tau Ceti (библиотека примерно на 3 миллиона строк, написанная ИИ и проверенная ИИ, теперь крупнее Mathlib), Formal Frontier (41 библиотека, около 200 тысяч строк) и реестр Palomar.

Предложенный план

Авторы прогнозируют, что большую часть математики можно формализовать за три года. Они предлагают курировать Mathlib, за считанные месяцы вырастить Tau Ceti и Formal Frontier в десять раз, написать дорожные карты, смоделировать затраты на масштабирование, оставить математиков в контроле над инструментами и организовать хостинг на некоммерческой или академической основе. Десять общих принципов включают ориентацию на Mathlib, публичную проверку и ссылки на литературу.

Что говорят работающие математики о проблеме объёма

Комментатор, который называет себя исследователем-математиком, описал то же давление с другой стороны:

«На прошлых выходных я набросал восемь статей. На этой неделе я не продвинулся ни в одной. ИИ застревает на ключевом месте задачи, по которой ещё мало работ… Архив arXiv завален. Человек не может оценить объём выдаваемого.»

Пользователь, который поручает Claude Code строить интерактивные объяснения, возразил, что это работает, только когда человек остаётся в цикле: «Это всё равно работа! И мне приходится изрядно повозиться, чтобы он выдал что-то осмысленное и красивое.»

Оба описывают узким местом ревью, а не генерацию. Это и есть аргумент поста Xena о том, кто будет проверять библиотеку, которая больше Mathlib.