陶哲轩牵头的Palomar开放提交：Lean证明有了登记处，但不是期刊

过去几个月，AI生成的数学证明数量猛增，不少还用Lean这种证明助手语言做了形式化。一个陌生的Github仓库声称证明了某个定理，读者很难判断它是真的证明对了，还是代码能跑但答非所问。

陶哲轩8月18日宣布，Lean FRO与ICARM孵化的Palomar登记处正式开放提交，专门收录通过Lean验证的数学形式化项目。他本人在科学顾问委员会里，同席还有Jeremy Avigad、Bryna Kra、Akshay Venkatesh。他自己提交的Sendov猜想证明形式化项目，成了这个登记处上线后的一个测试案例。

Palomar怎么给证明“过检”

Palomar的登记流程很具体。提交者先固定一个Github commit快照，代码之后再改，也不影响这次登记的结果。

两项都通过，项目才会挂到登记处上，随附challenge file、solution module和formalization.yaml等元数据，方便后来者复核。

机械验证不是学术认证

Sendov猜想这个案例说明问题所在。代码通过Comparator检查，只证明了“这段Lean代码逻辑自洽”，不代表Sendov猜想的证明完成了同行评审，也不代表这项结果的新颖性和重要性得到数学界确认。

陶哲轩在公告里写得很直白：Palomar的检查“远远不及”人工同行评审对新颖性、重要性和准确性的把关，Palomar“不是”peer-reviewed journal。

这个区分对读者有实际意义。被登记的证明，Lean代码经过了工具验证，不再是随便扔在某个仓库里没人核实过的东西。但登记本身不背书这个结果是不是重要突破，LLM那道语义检查也只是“看起来匹配”，出错的可能性一直都在。

更像预印本库，对谁意味着什么

拿传统数学出版流程做对照更清楚。

Palomar卡在两者中间：比预印本多一层机械可核验性，比期刊评审浅得多。

对使用AI或Lean做形式化的研究者，Palomar给了一个规范化的发布入口。提交前先锁定commit快照，通过Comparator检查基本没有争议，卡壳的地方多半出在LLM语义匹配这一步——陈述写得越贴近自然语言原文，通过概率越高。

对需要判断某个AI证明可不可信的数学读者和从业者，实际动作分两步：先看有没有通过Palomar的两道机械检查，这一步能筛掉明显造假或文不对题的代码；再决定要不要花时间去读证明本身、判断它是否值得关注，这一步Palomar帮不上忙，还得靠自己或等同行评审。

陶哲轩提到打算把更多旧的形式化项目陆续提交上去，说明这个登记处目前处于习惯养成期。规模、提交量、通过率这些数字，原文都没有给出，值不值得当作行业标配还看不清楚。

接下来值得盯的，是数学圈会不会真把“通过Palomar登记”当成评估AI证明可信度的一道及格线，还是仅仅当技术性存档工具用。