前几天刷到陶哲轩 8 月 18 日的博客，说 Palomar 登记处正式开始接受 Lean 验证数学成果的提交了。这个东西由 Lean FRO 和 ICARM 孵化，定位类似一个面向 Lean 证明的预印本服务器，登记的是外部 GitHub 仓库的特定提交快照，不替你保管代码。对数学界意味着什么那种大话题轮不到我，这篇只记两个我拆开看看之后觉得值得记的细节：提交的文件结构，以及它用 LLM 做的那一步检查。说实话后者才是我点进去的原因。
先说文件结构，这部分顺手就能过一遍。每个提交的仓库要放三样东西：一个挑战文件（statement，简短的 Lean 描述）、一个解决方案模块（证明本体）、一个 formalization.yaml（元数据，里面含非正式的自然语言描述）：
repo/
├── statement.lean # 挑战文件
├── solution.lean # 证明
└── formalization.yaml # 元数据 + 非正式描述
然后 Palomar 的检查分两层。第一层是确定性的：用 Lean 工具 Comparator 检查解决方案模块是否类型检查通过、并且精确证明了挑战文件里的声明。这一层没什么可展开的，Lean 自己就是裁判。第二层才是有意思的地方：它用大型语言模型去检查 formalization.yaml 里的非正式描述和挑战文件里的形式化声明是不是一回事。
为什么这一步有意思。形式化证明最经典的坑从来不是证明本身错，而是“证明的那个命题”和“你以为它证明的那个命题”对不上——statement 写偏了一个量词、一个边界条件，证明照样类型检查通过，但登记上去的东西和论文里那句人话是两回事。以前这个对齐只能靠人肉眼抠，现在 Palomar 把它做成了流程里的一道关卡，而且老实承认这道关卡用的是 LLM。我第一反应也是“LLM 检查靠谱吗”，这个反应到现在也没完全放下，但后来想明白了一件事：这一步检查的对象本来就是自然语言和形式语言之间的翻译质量，而翻译对不对这件事，人类审稿人自己也只能凭语感。LLM 在这里不是替掉了一个严谨环节，是替掉了一个从来就不严谨的环节——真正严谨的那部分（证明对不对）从头到尾都归 Lean 管。想明白这一层之后我对这个设计的抵触小了很多，虽然“从来就不严谨”不等于“可以随便交给机器”，这个区别我还没完全想透，先记着。
陶哲轩在公告里专门强调了一句：Palomar 的检查不属于人类同行评审，不评估新颖性、学术兴趣或准确性。我特别欣赏他把这条写在前头。预印本服务器的历史包袱就是总有人拿 arXiv 挂名当背书，一个只做机器检查的登记处如果不说清楚自己不做什么，迟早也会被这么用。把边界划在“我只保证这个证明证明了这条 Lean 声明、这条声明大致对应你写的这段人话”，剩下的概不负责——这个诚实的收缩反而让整个系统可信。我见过太多工具在宣传里把自己说得无所不能，真用起来才发现每条承诺都要打折扣，反着来的反而让人踏实。
另外一条：它现在对人类生成、AI 生成和混合生成的提交一视同仁。陶哲轩自己已经把 Sendov 猜想的 Lean 形式化证明提交上去了，还计划把更早的形式化成果陆续补登。混合生成这个口子开得很自然，毕竟 2026 年了，纯手写的证明越来越少，而 Palomar 的立场从头到尾一致：它不关心证明怎么来的，只关心机器能不能验。这个立场我认，和我一直记在笔记里的那条是同一件事——看不懂的代码不能用，能验的证明才作数，来源反而没那么要紧。
这里留一个坑：Comparator 我还没实际跑过，LLM 那层检查的具体 prompt 和判定标准对外能看到多少，我还没翻到，翻到之后打算另起一篇补上。另外我很好奇 LLM 检查给出“不匹配”时的申诉流程长什么样——自然语言对齐这种事，误判几乎是必然发生的，一个登记系统的成色往往就体现在它怎么处理误判。这两个问题现在都没有答案，我不想猜了写上去装作搞懂了。
划重点：第一，Palomar 的检查分两层，Lean 管证明对不对，LLM 管形式化声明和非正式描述对不对，两层管的不是同一件事；第二，LLM 检查翻译对齐不算用 AI 替代严谨性，因为这一环从来没有严谨过；第三，它明说自己不做同行评审、不评新颖性，这个边界声明本身就是设计的一部分。这篇就记到这里，你可以去翻一下陶哲轩那篇公告原文，再点进 Palomar 看一个已登记条目的仓库结构，比看十篇转述都有用。