Теренс Тао: реестр Palomar принимает проверенные Lean-доказательства
На своём блоге математик Теренс Тао объявил об открытии Palomar, реестра доказательств, формализованных на языке проверки Lean, для приёма заявок. Проект инкубирован Lean FRO и ICARM; Тао входит в научный консультативный совет реестра вместе ещё с восемью математиками: Джереми Авигадом, Мэттью Баллардом, Хаумой де Диосом, Нестором Гильеном, Бриной Кра, Ким Моррисон, Рави Вакилом и Акшеем Венкатешем.
Поводом стал рост числа доказательств, сгенерированных ИИ, как новых, так и переформулировок старых результатов, часть из которых формализуют на Lean. Проверить, что конкретный Lean-репозиторий действительно доказывает заявленное утверждение, непросто, особенно для тех, кто не владеет Lean: нужно убедиться, что формальные утверждения действительно типизируются и доказываются, что в доказательстве нет «читов» вроде добавления лишних аксиом, и что формальная запись по смыслу совпадает с неформальным описанием результата. Palomar задуман как аналог сервера препринтов, но для Lean-доказательств: это реестр внешних GitHub-репозиториев (точнее, их «снимков», конкретных коммитов), оформленных по текущим лучшим практикам формализации.
Каждая заявка должна содержать три элемента: «challenge file», короткое, читаемое человеком описание заявленного результата на Lean; «solution module», собственно доказательство произвольной длины; и файл «formalization.yaml» с неформальным описанием результата и дополнительными метаданными. К репозиторию предъявляются и другие технические требования, которые в посте не раскрываются.
Заявка проходит две проверки. Первая, чисто механическая: инструмент Comparator подтверждает, что модуль решения типизируется и доказывает ровно то, что заявлено в challenge file. Вторая, недетерминированная: большая языковая модель оценивает, соответствует ли неформальное описание из formalization.yaml заявленному результату. Если репозиторий проходит обе проверки и минимальные требования к оформлению, его регистрируют в Palomar. Тао подчёркивает: обе проверки заведомо слабее полноценного человеческого рецензирования на новизну, интерес и точность, Palomar не рецензируемый журнал.
В качестве теста Тао сам успешно подал в Palomar собственную недавнюю формализацию доказательства гипотезы Сендова и планирует в ближайшее время отправить туда и более старые формализации. Реестр открыт для формализаций как старых, так и новых результатов; принимаются заявки, сделанные человеком, ИИ или в смешанном режиме, при этом Тао отмечает, что современные ИИ-агенты заметно помогают с механической частью оформления заявки, хотя человеческую проверку он всё равно настоятельно рекомендует. Обсуждение и обратную связь по Palomar предложено вести в отдельном канале Zulip.
Ключевые факты
- Palomar, новый реестр доказательств, формализованных на языке Lean; инкубирован Lean FRO и ICARM, сейчас открыт для приёма заявок
- В научный консультативный совет реестра входят девять математиков, включая Теренса Тао, Джереми Авигада, Рави Вакила и Акшея Венкатеша
- Заявка обязана включать три файла: challenge file (формальная постановка задачи на Lean), solution module (доказательство) и formalization.yaml (неформальное описание)
- Проверка двухступенчатая: механический инструмент Comparator подтверждает, что доказательство типизируется и закрывает ровно заявленное утверждение, а LLM отдельно оценивает соответствие неформального описания формальному
- Palomar, не рецензируемый журнал: обе проверки слабее полноценного человеческого рецензирования, Тао сам протестировал систему, подав туда свою формализацию доказательства гипотезы Сендова
Почему это важно
Формализованные на Lean доказательства в последние месяцы стали появляться в больших количествах, их всё чаще генерируют ИИ-модели, но у сообщества не было единого места, где такие доказательства можно зарегистрировать и хотя бы механически проверить. Palomar закрывает именно этот пробел: он играет для Lean-доказательств роль, похожую на роль сервера препринтов, задаёт общий формат подачи (challenge file, solution module, formalization.yaml) и прогоняет каждую заявку через автоматическую проверку корректности.
Кому это важно
В первую очередь тем, кто формализует математику на Lean, авторам-людям, командам, использующим ИИ-агентов для формализации, и математикам, которым нужно быстро понять, доказывает ли чужой Lean-репозиторий то, что заявлено. Появление реестра также важно для более широкого круга исследователей ИИ, которые следят за тем, как формальная верификация может стать проверкой качества для ИИ-генерируемых доказательств.
Как это применить
Подать заявку в Palomar может кто угодно, инструкции по формату (challenge file, solution module, formalization.yaml) выложены отдельно, и, по словам Тао, современные ИИ-агенты заметно облегчают техническую часть оформления. При этом заявка не заменяет рецензирование: перед подачей Тао рекомендует человеческую проверку, а обсуждать вопросы и получать обратную связь предлагается в отдельном Zulip-канале проекта.
Можно ли доверять
Прохождение Palomar подтверждает только то, что доказательство типизируется в Lean без «читов» вроде лишних аксиом и что его неформальное описание, по оценке LLM, похоже на заявленный результат, то есть корректность формальной записи и её соответствие постановке задачи, но не оценку новизны, значимости или качества результата. Тао сам прямо оговаривает: Palomar, не рецензируемый журнал, и обе проверки заведомо слабее полноценного человеческого рецензирования.
Риски и подводные камни
Вторая проверка, соответствие формальной записи неформальному описанию, выполняется языковой моделью и по определению недетерминированная, то есть может ошибаться в обе стороны. В посте не раскрыто, что происходит с заявкой, провалившей проверку, сколько заявок уже подано и какие ещё технические требования предъявляются к репозиторию помимо перечисленных трёх файлов, эти детали остаются за кадром анонса.
«Стоит подчеркнуть: проверки (a) и (b) заведомо слабее полноценного человеческого рецензирования заявки на новизну, интерес и точность, в частности, Palomar не рецензируемый журнал.»
— Теренс Тао, в объявлении о запуске Palomar