18 августа 2026 Теренс Тао объявил на своем блоге об открытии Palomar (palomar-registry.org) — реестра математики, верифицированной на языке проверки типов Lean, который он сам описывает как «препринт-сервер для Lean-доказательств». Реестр открыт для подачи снимков публичных репозиториев с Lean-доказательствами; инициативу вырастили Lean FRO и исследовательский институт ICARM.

Что произошло

В научный совет реестра входят Тао, Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Ravi Vakil и Akshay Venkatesh. В Palomar принимаются снимки публичных GitHub-репозиториев за конкретный коммит, содержащие Lean-код: challenge file с читаемым утверждением, solution module с доказательством любой длины и файл formalization.yaml с неформальным описанием, метаданными и раскрытиями. Снимок регистрируется только после трех автоматических проверок без участия человека: инструмент Comparator проверяет, что код проходит типизацию и доказывает ровно заявленное утверждение против зафиксированной версии Mathlib и whitelist разрешенных аксиом, независимая LLM сверяет формальное и неформальное утверждения, а третий уровень аудиторит раскрытия в formalization.yaml. Первая запись реестра уже зарегистрирована — это доказательство гипотезы Сендова с идентификатором PALOMAR-2026-08-13-000001, формализация которого приписывается Тао.

Контекст

Lean — язык проверки типов, позволяющий формализовать математические утверждения в виде кода и проверить доказательство механически, а библиотека Mathlib служит основой, против которой в реестре сверяются доказательства. По формату Palomar близок к препринт-серверу в духе arXiv, но отличается механизмом доверия: до регистрации материал проходит машинную проверку, после чего результат становится цитируемой записью с уникальным идентификатором. Реестр прямо не является журналом: он разделяет «proof of the statement» и peer review, поэтому новизна и значимость результата не входят в автоматическую проверку. Контекст появления проекта — лавина формализованных ИИ-доказательств, которые неспециалисту непросто проверить: до появления такого реестра утверждение о машинопроверенном доказательстве было трудно подтвердить без глубокой экспертизы в коде Lean.

Почему это важно для индустрии

Для отрасли Palomar — не продукт, а инфраструктурный стандарт доверия к машинопроверенным результатам: воспроизводимый протокол проверки и публичный цитируемый датасет верифицированных теорем. Для билдеров это открывает новую поверхность — end-to-end агентный воркфлоу «сформулировал — сформализовал — сдал в реестр» и инструментарию вокруг формализации: агенты, пайплайны, поиск и интеграции. Стандартизационный сигнал значителен: механизм доверия к машинопроверенным результатам зафиксирован на вершине дисциплины (Тао, ICARM/NSF, Lean FRO), и будущие продукты «ИИ-доказательств» будут оценивать по критерию, можно ли их результат сдать в реестр. Динамика зарегистрированных записей со временем может стать публичным индикатором роста возможностей ИИ в теоремодоловании.

Почему это важно для пользователей

Реестр публичный и searchable, с фильтрами по Mathlib, arXiv и MSC: любой читатель может посмотреть, какие результаты уже прошли проверку. Инструмент Comparator и стандартный формат formalization.yaml доступны для изучения, инструкция по сабмишен публична на странице palomar-registry.org/how-to-submit, и при желании можно подать собственную Lean-формализацию. По словам Тао, современные AI-агенты хорошо помогают с механикой сабмишена. Обсуждение реестра идет в Palomar-канале на Lean Zulip.

Что пока неизвестно / ограничения

При чтении результатов реестра стоит учитывать несколько оговорок. Второй уровень проверки — соответствие формального и неформального утверждения — выполняет LLM, а не формальный метод, поэтому ошибка формализации (Lean-утверждение шире или уже неформального описания) может пройти проверку. Входом для третьего уровня — аудита раскрытий в formalization.yaml — служит самоотчет сабмитента, и то, насколько машина способна проверить честность self-disclosure, в заявлении не раскрыто. Низкий порог входа масштабирует поток ИИ-сгенерированных подач, а легкость сабмишена самой по себе не является гарантией качества результата.

Источники

Автор

Look at AI, редакция