Palomar：一个Lean验证数学的注册库

# Palomar – 一个Lean验证数学的注册平台 来源：https://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/ 近几个月来，AI生成的各类新旧定理证明数量激增，其中一些已在证明辅助语言Lean中形式化。然而，检查某个Lean代码库是否确实证明了所声称的命题并非易事，尤其对于不熟悉Lean使用的受众：首先需要验证形式化的Lean命题是否存在可通过类型检查的证明，确保证明未包含添加额外公理等“作弊”行为，同时确认形式化表述在语义上符合命题的非形式化描述。 为帮助厘清现状，我很高兴宣布Palomar——一个Lean验证数学注册平台（https://palomar-registry.org/）现已开放提交。该平台由Lean FRO（https://lean-lang.org/fro/）与ICARM（https://icarm.io/）联合孵化。我将在此平台担任多项职务，包括与其他科学顾问委员会成员Jeremy Avigad（https://www.andrew.cmu.edu/user/avigad/）、Matthew Ballard（https://www.matthewrobertballard.com/）、Jaume de Dios（https://jaume.dedios.cat/）、Nestor Guillen（https://www.ndguillen.com/）、Bryna Kra（https://en.wikipedia.org/wiki/Bryna_Kra）、Kim Morrison（https://tqft.net/）、Ravi Vakil（https://math.stanford.edu/~vakil/）及Akshay Venkatesh（https://www.math.ias.edu/~akshay/）共同参与。 Palomar的详细设计动机可在此处查阅（https://palomar-registry.org/statement），更多信息可访问此处（https://palomar-registry.org/about）。Palomar的初步定位可类比为Lean证明的预印本服务器。更准确地说，Palomar（得名于帕洛马天文台（https://sites.astro.caltech.edu/palomar/homepage.html））是一个注册平台，收录外部GitHub仓库（或更准确说是这些仓库的“快照”，以特定GitHub提交为表示）中遵循当前最佳形式化实践的Lean代码，具体包含： - 包含命题非形式化简短描述的“挑战文件”（用Lean编写） - 包含挑战文件中命题任意长度证明的“解答模块” - 用非形式化语言描述命题并包含相关元数据与声明的“formalization.yaml”文件 （仓库还需满足其他技术要求，此处不赘述。）当仓库快照提交至Palomar时，系统将进行双重检查：（a）验证解答模块能通过类型检查并恰好证明挑战文件中的命题；（b）确认formalization.yaml中的非形式化描述与挑战文件中的命题相符，同时验证仓库满足注册条目的各项基本标准。第一项检查（a）完全通过Lean工具Comparator（https://github.com/leanprover/comparator）机械执行；第二项检查（b）则由大语言模型非确定性完成。通过两项检查的仓库即可在Palomar注册。需特别强调的是，（a）（b）项检查远未达到人类同行评审对提交内容新颖性、价值性与准确性的评估标准；Palomar**并非**同行评审期刊。 提交流程虽严谨但可操作：作为测试，我已成功将自己近期形式化的Sendov猜想证明（https://github.com/teorth/sendov）提交至Palomar，未来还计划将一些早期形式化成果注册到该平台。 总之，该注册平台现已开放接受新旧定理的形式化成果。欢迎人类生成、AI生成或两者混合生成的提交；请在开始前仔细阅读（相当详细的）提交指南（https://palomar-registry.org/how-to-submit）。（需说明的是，现代AI助手确实能协助处理提交的机械性细节，但仍强烈建议进行人工复核。） 关于Palomar的讨论与反馈可在Zulip频道（https://leanprover.zulipchat.com/#narrow/channel/621638-Palomar）进行。