Palomar 为 AI 数学堆积开放了一个 Lean 证明注册库
该项目登记固定的 GitHub 快照，以机械方式检查 Lean 证明，并使用 LLM 将形式化陈述与非正式描述进行比较。
By RuntimeWire Staff · Published
Primary source: Terence Tao
Why it matters
Palomar gives Lean proofs fixed, commit-level records and separates mechanical verification from semantic LLM review. Its narrow scope provides researchers with an audit trail while explicitly stopping short of peer review.
Palomar 于 8 月 18 日开放提交，为数学家提供了一个公共注册库，其中用 Lean 编写的形式化证明可以与固定的源代码快照关联、被机械性地检查，并在初次公告过去后仍可被检视。
Terence Tao，这位 UCLA 的数学家、2006 年菲尔兹奖得主，在一篇博文中宣布了该平台的开放。Tao 是 Palomar 四位初始技术维护者之一，其他维护者包括 Matthew Ballard、Nestor Guillen 和 Jaume de Dios Pont。该项目由 Lean Focused Research Organization 和 Institute for Computer-Aided Reasoning in Mathematics (ICARM) 孵化。
Tao 将该项目定位为对大量 AI 生成证明（其中一些已在 Lean 中形式化）激增的回应。他写道，对于没有 Lean 专业知识的读者来说，审查这些仓库仍然困难：证明必须通过类型检查、避免未授权的公理，并在形式上陈述与普通数学语言所描述的相同结果。
Palomar 的做法是为固定仓库快照所证明的内容创建一条注册记录。Tao 将其描述为面向 Lean 证明的预印本服务器的“零阶近似”。这一比喻设定了正确的预期：Palomar 创建了可索引的成果物和审计线索，但并不对数学内容进行审稿。
Tao 的参与为该工作带来了可见度，尽管 Palomar 的运营结构是分布式的。Ballard 是 University of South Carolina 的代数几何学家。Guillen 的研究方向包括偏微分方程、变分法和科学计算。De Dios Pont 于 2023 年在 Tao 指导下完成 UCLA 博士学位，目前是 NYU Center for Data Science 的教员研究员，从事与 AI 在数学中的应用相关的工作，同时研究调和分析和谱理论。更广泛的科学顾问委员会还包括 Jeremy Avigad、Bryna Kra、Kim Morrison、Ravi Vakil 和 Akshay Venkatesh。
Palomar 实际检查的内容
Tao 的发布文章将 Palomar 描述为外部 GitHub 仓库快照（由特定提交表示）的注册库。每次提交包括一个简短的 Challenge.lean 文件，陈述所声称的结果；一个包含证明的 Solution.lean 模块；以及一个包含非正式描述、元数据和披露信息的 formalization.yaml 文件。
机械性检查使用 Comparator，这是一种将所宣称的定理陈述与其证明分离开来的 Lean 工具，并检查该解是否在挑战文件中确立了该结论。Lean 的文档指出，Comparator 支持定理陈述匹配，并且可以使用 Lean 的内核和独立实现的 Nanoda 检查器。现有材料并未证明 Palomar 要求使用所有 Comparator 的验证选项。
这种分离解决了一个微妙的失效模式：一个仓库可能包含一个有效证明，但其形式化陈述与代码之外描述的定理不同。将挑战陈述与解分开，能让读者需要检查的表面更小。
Palomar 的第二项检查是非确定性的。根据 Tao 的公告，一个大型语言模型会评估 formalization.yaml 中的非正式描述是否似乎与形式化结果相匹配，以及该仓库是否满足注册库的最低标准。
Palomar 的已发布政策描述了自动化的注册审查，但提供的材料并未说明维护者是否另外进行人工审核。Tao 也建议在提交过程中进行人工审查，并表示 Palomar 的检查远不足以替代针对新颖性、重要性和准确性的同行评审。
因此，该注册库将机械证明检查与基于模型的评估结合起来，以桥接 Lean 代码与普通数学语言之间的语义差距。项目文档也警告说，语言模型的审查可能会遗漏不一致之处。读者仍然需要检查定义和形式化陈述是否捕捉了所讨论的定理。
验证而非背书
Palomar 在其声明上划定了明确的界限。注册并不认证新颖性、重要性、代码质量或非正式证明的正确性。它不意味着专家评审已经审阅该工作，也不将 GitHub 仓库转变为期刊出版物。
有用的声明是狭义的：来自指定仓库快照的一个证明通过了 Palomar 已记录的机械和自动化检查。随后，挑战文件、解答和随附说明为其他研究者提供了可供检视和质疑的材料。
随着 AI 辅助形式化的传播，这一区别变得重要。证明检查器可以判断代码在其编码的假设下是否确立了一个形式化陈述。而一个公开的数学主张还取决于该陈述、其定义以及非正式描述是否指向相同的结果。
Tao 和 Palomar 的维护者们正在为这一第二层构建基础设施，同时刻意限制注册库的声明范围。Palomar 目前支持 Lean，提交可以是人工生成、AI 生成，或两者混合产生。
Palomar 不会为机器生成数学是否成立的争论给出定论。它为这些争论提供了固定的仓库快照和明确的可检验主张——在一个已经在应对自动化证明激增的领域中，这是一项有用的基础设施。