Три года назад автор заметки на MathOverflow в неформальной беседе с коллегами предположил, что математическое сообщество ещё может успеть централизованно выбрать эталонный proof assistant. Сейчас это кажется почти решённым: Lean набрал колоссальную инерцию благодаря Xena Project Кевина Баззарда, Liquid Tensor Experiment Петера Шольце, а позже и самостоятельному изучению Lean Терри Тао. Конвертация Mathlib с 3-й на 4-ю версию едва завершилась, и как раз запустили Lean FRO — момент, когда Lean ещё не выглядел столь неизбежным, был упущен.
Теперь автор ставит вопрос иначе: есть ли шансы на серьёзную институциональную поддержку альтернативы вроде Metamath? В пользу Metamath говорит два обстоятельства. Во-первых, интерактивные proof assistant’ы (ITP) нужны математикам, чтобы формально проверять доказательства — и человеческие, и сгенерированные AI. У Lean уже находили soundness-баги, а поиск малозаметных ошибок такого рода — конёк AI. Благодаря работе Марио Карнейро над Metamath Zero гарантии корректности у Metamath оказываются заметно выше. Во-вторых, Metamath построен на теории множеств, а не на изоморфизме Карри–Говарда «предложения как типы», и тем самым снимает часть концептуальных проблем, о которых недавно писал Джеймс Хэнсон на MathOverflow. Похожие позиции занимают Mizar и Isabelle/ZF, но у них нет аналога Metamath Zero.
Автор подчёркивает, что не привязан именно к Metamath, и не призывает бросать Lean — у того прекрасное сообщество и много достоинств. Однако популярность Lean, по его мнению, во многом объясняется выбором нескольких ярких фигур, а не объективным превосходством. Главный козырь Lean — Mathlib. Её полное воспроизведение для другого ITP ещё недавно казалось нереалистичным, но нынешние AI-модели уже способны на генерацию формальной математики. Код, написанный AI для Lean, пока не дотягивает до качества Mathlib, и для Metamath результат будет не лучше, но сама идея создать жизнеспособную библиотеку перестала быть абсурдной. Без институциональной поддержки, однако, такой проект не взлетит, а её источник пока неизвестен.
В конце автор уточняет: он работает на подрядчика правительства США, но все высказанные соображения — сугубо личные. Никто в официальных структурах не выражал недовольства Lean и не требовал альтернатив. Три года назад на его неформальный доклад никто не отреагировал, и сейчас он не ждёт иного.