Palomar 开放面向 Lean 验证数学的公共注册库

发生了什么？

2026 年 8 月 18 日，Palomar 作为 Lean 验证数学的公共注册库开放投稿，由 Lean Focused Research Organization 与 ICARM 共同孵化。每个注册结果都绑定固定的公开 源码版本，并记录精确形式陈述、依赖和验证元数据。Palomar 使用 Comparator 分离 statement 与 proof 并重放证明，同时通过 Lean kernel 与 NanoDa 再检查导出的证明， 要求提交 formalization.yaml provenance 信息，并加入自动语义审查；注册本身不被 表述为对新颖性或数学重要性的认证。

Palomar 的设立背景是 machine-assisted / machine-generated mathematics 数量快速增加， 而成果分散在代码仓库和公告中，外部读者难以核查。其公开声明把该服务定位为形式化成果 的 preprint / repository 层：提供不可变、可搜索、可检查的机械验证记录，同时把新颖性、 相关性和更深层数学判断留给研究共同体。

为什么重要？

单纯的形式证明检查不能保证公开形式定理忠实表达非形式研究主张，一个代码仓库链接也不能 自动形成稳定学术记录。Palomar 明确这些边界，并把 statement identity、proof replay、 AI 使用披露和源码固定版本转化为可复用基础设施，以适应高产量 AI 辅助形式化时代。

重要性说明：Palomar 构成领域级里程碑，因为它为固定源码版本上的 Lean 验证研究成果建立了持续性的 制度与技术注册基础设施。其工作流把 proof replay 与语义、provenance 审查分离， 公开精确定理陈述和依赖关系，并直接回应 AI 辅助及 AI 生成形式数学快速增长带来的 记录与核验问题。该注册库显著组织了领域实践，但并不声称替代数学同行评议或认证新颖性。

历史脉络

主要证据

• Palomar: a registry of Lean-verified mathematics
  S2 · 官方机构来源 · 官方公告 · 2026-08-18
• Palomar – a registry of Lean verified mathematics
  S2 · 官方机构来源 · 社区来源 · 2026-08-18