2026 年 8 月 18 日，陶哲轩（Terence Tao）在个人博客宣布，Lean 验证数学注册表 Palomar 正式开放提交。这个由 Lean FRO 与 ICARM 共同孵化的项目，瞄准的是 2026 年以来日益尖锐的一个问题：AI 生成的数学证明数量激增，但确认一个 Lean 仓库真的证明了它声称的结果，对非 Lean 专家来说异常困难。
陶哲轩把验证难题拆成三层：首先要确认被声称的形式化陈述确实有通过类型检查的证明；其次要确认证明没有作弊，比如偷偷添加额外公理；最后还要确认形式化陈述与结果的非形式描述在语义上真的对得上。三层里任何一层出问题，一个看起来漂亮的形式化都可能名不副实。
一条注册条目长什么样
Palomar 的名字来自帕洛玛天文台（Palomar Observatory），定位接近 Lean 证明的预印本服务器。它登记的是外部 GitHub 仓库的快照，即绑定到一个具体 commit 的不可变版本。每个提交必须包含三个组成部分：
- Challenge.lean（挑战文件）：用 Lean 写成的、人类可读的结果陈述；
- 解决模块（solution module）：任意长度的证明本体；
- formalization.yaml：用自然语言描述结果，并携带来源、协作、AI 使用等元数据。
formalization.yaml 是 Mathlib Initiative 推出的标准，专为形式化证明设计。它有字段记录与原始非形式证明作者的合作、AI 的使用情况（包括模型和预算）、以及许可、引用、署名层面的合规情况。一个形式化项目用了哪个模型、花了多少预算，都以结构化方式记录在案。
条目通过检查后，Palomar 用 Lean FRO 的文档系统 Verso 把主定理渲染成网页，鼠标悬停即可查看 Lean 术语的含义，读者可以直接看到被验证的确切陈述。
两道检查：机械与语义
提交进入注册表需要过两道全自动检查，中间没有人类编辑环节。
第一道是纯机械的。Lean FRO 开发的 Comparator 工具把陈述和证明放进独立沙盒分别编译，用 lean4export 导出两套环境，确认陈述所依赖的声明在两边完全一致，防止证明悄悄弱化它声称建立的命题。导出的证明随后要经过两套内核的重放：Lean 自带内核，加上独立实现的 NanoDa 内核。NanoDa 用 Rust 编写，不共享 Lean 内核代码，能抓住一类两种 Lean 侧检查都抓不住的问题：一个篡改 elaborator 状态的元程序骗得过 Lean 的第一遍检查，骗不过独立内核。Comparator 还强制被比较的定理不使用配置允许清单之外的公理，而这份配置本身要过 Palomar 的策略校验。
第二道检查由大语言模型执行，判断 Challenge.lean 里的形式陈述是否公平地表达了 formalization.yaml 等处给出的非形式数学主张。这里设有一道编辑门槛（editorial floor），模型要回答两个问题：这个结果是否可能支撑一篇研究论文或严肃的研究笔记；能否识别出一个可信的研究方向，以及一个可能觉得它有趣或相关的研究者类型。LLM 使用的提示词、运行方式与必须产出的报告，全部公开发布在 PalomarPolicy 仓库。
评审在这个体系里是一个过滤器：它可能识别出阻断性问题，也可能没有发现阻断性问题，但它不接受、不批准、不背书任何结果。提交者可以看到私有评审报告，自行决定注册还是撤回。
一个有意思的细节是分数的处理。同一个仓库同一个 commit 曾在两次评审中的某一轴上先后得到 5 分和 4 分，注册资格结论两次相同。组织者的判断是，一个会这样波动的数字撑不起判断的分量，因此对外只公布是否发现阻断性问题，分数本身被刻意保留。
边界：它不做什么
Palomar 的 About 页用 11 条否定式声明划清边界，关键几条包括：
- 形式认证不绝对：验证在安全沙盒中尽最大努力进行，但所用 Lean 内核、Mathlib 缓存与工具链本身可能存在 bug 或漏洞，独立验证的需求并未取消；
- 不保证形式结果与非形式结果的完全对齐：LLM 会生成详细差异报告，但模型可能出错，报告只辅助读者自行核对；
- 不验证非形式证明本身，不评估代码质量；
- 不是新颖性证书，也不是重要性证书，编辑门槛只说明存在可信的受众；
- 不执行同行评审，不是期刊，注册不构成发表，也不是向期刊投稿或向 Mathlib 提交代码的绿灯；
- 是注册表而非仓库：数学内容留在原 GitHub 仓库，条目只记录对某个 commit 的主张，另存一份公共保存 fork 作为备份。
条目绑定完整 40 位 commit 哈希，被验证的工件不会漂移。Lean 或 Mathlib 更新后，已有条目不会重新运行，不会因此升级或失效。要登记新版本，需要提交新的 commit 并从头通过全部检查，成为同一 Palomar ID 的下一个版本，旧版本永久可解析。
陈述文件的规模有硬性上限：1000 行、100 KiB。陈述的导入限定在 Lean core、Mathlib 与 Tau Ceti，Tau Ceti 依赖会在条目上标记；证明侧的依赖不受此限，可以是任意固定的 Git 仓库。注册表元数据以 CC0 发布并提供 feed，任何人都可以在数据之上构建评论或索引层。
治理与首批条目
项目的治理分三个角色：技术维护者（初始为陶哲轩、Matthew Ballard、Nestor Guillen、Jaume de Dios）管理仓库与线上服务；仲裁者（Moderators）可批准个别版本的撤回或恢复；科学顾问委员会（成员包括陶哲轩、Jeremy Avigad、Matthew Ballard、Jaume de Dios、Nestor Guillen、Bryna Kra、Kim Morrison、Ravi Vakil、Akshay Venkatesh）就政策与标准提供咨询，不审查具体提交。
注册页面显示已收录 10 条结果、9 个源项目。编号 PALOMAR-2026-08-13-000001 的第一条，是陶哲轩本人提交的 Sendov 猜想形式化：当复多项式的所有零点都落在闭单位圆盘内且次数至少为 2 时，原多项式的每个零点，距离导多项式 p' 的某个零点不超过 1。
其他已注册条目包括 rkirov/jordan_pick（Jordan 曲线定理：圆到平面的连续单射，其余集恰有两个连通分支；证明沿 Maehara 的路线归约到 Brouwer 不动点定理）、AxiomMath/PrimeGapsLib、gexahedron/sabidussi-lean、Paul-Lez/hadamard-668-comparator、kim-em/erdos-unit-distance-comparator 等。陶哲轩在公告中提到，现代 AI agent 能有效协助提交流程中的机械性细节，但仍强烈建议人工复查。
给生态留下什么
Palomar 的 statement 页对背景的描述相当直接：新闻稿、社交媒体帖子与公司网站不足以承载一个数学形式化成果的记录。2026 年以来机器辅助证明的数量和复杂度大幅上升，未经审查的重大声称每天都在出现，这种情况正在侵蚀「已确立的数学事实」的既有标准，而数学界需要一套社区公认的最低标准，并尽可能用自动工具校验执行。
设计者希望注册表成为传统期刊的基础设施：期刊可以把 Lean 形式化纳入编辑流程，让作者先在 Palomar 登记；形式化提供的机械正确性保证，则让审稿人把稀缺时间花在新颖性与优雅度上，避免在基础逻辑层面消耗精力。statement 页同时点明态度：数学界必须保住设定标准的中心角色，避免标准在野外自生自灭，或被与数学发展利益冲突的外部方强加。
对 AI for Mathematics 方向的研究者，Palomar 提供的是一个可引用的锚点：一个形式化成果从 GitHub 仓库、公司博客或推文线程，变成可检索、可比对、带不可变版本记录的登记条目。formalization.yaml 中的 AI 使用披露，也让「这个证明有多少是模型生成的」拥有了机器可读的记录，不再停留在口头发言层面。