🏛️ Palomar: Теренс Тао открыл реестр проверенных Lean-доказательств
18 августа 2026 на своем блоге Теренс Тао объявил, что Palomar (palomar-registry.org) — «препринт-сервер для Lean-доказательств», реестр математики, верифицированной на языке проверки типов Lean, — открыт для приема работ. Инициативу вырастили Lean FRO и ICARM (NSF Mathematical Sciences Research Institute при Carnegie Mellon University); в научный совет, помимо Тао, вошли Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Ravi Vakil и Akshay Venkatesh.
🌍 На фоне растущего потока формализованных, в том числе полученных с помощью ИИ, доказательств Palomar задает инфраструктурный стандарт доверия к машинопроверенной математике: снимок конкретного коммита публичного GitHub-репозитория регистрируется только после трех автоматических проверок без участия человека. Инструмент Comparator (github.com/leanprover/comparator) механически проверяет, что решение типизируется и доказывает ровно заявленное утверждение против зафиксированной версии Mathlib с разрешенным списком аксиом, LLM сверяет, что формальное утверждение честно передает неформальное описание, а третий этап аудитует раскрытия в formalization.yaml. Реестр явно не является журналом и разделяет «proof of the statement» и peer review, но дает устойчивые цитируемые записи о формализованных теоремах. В качестве теста Тао подал свою недавнюю формализацию доказательства гипотезы Сендова (запись PALOMAR-2026-08-13-000001); принимаются и старые, и новые результаты — доказанные человеком, ИИ или смесью обоих.
👤 Реестр публичный, поиск идет с фильтрами по Mathlib, arXiv и MSC, а обсуждение — в Palomar-канале на Lean Zulip: можно посмотреть, какие результаты уже прошли проверку, и изучить инструменты Comparator и формат formalization.yaml. Подать свою Lean-формализацию можно по инструкции на palomar-registry.org/how-to-submit — по словам Тао, с механикой подачи хорошо помогают современные AI-агенты.
Источник 1: https://terrytao.wordpress.com/2026-08-18/palomar-a-registry-of-lean-verified-mathematics/ Источник 2: https://icarm.io/news/announcing-palomar-a-registry-of-lean-verified-mathematics/