Palomar Registry Launches as a Preprint Server for Lean‑Verified Mathematics

Palomar provides a lightweight, automated gatekeeper for Lean formalizations

Palomar 是一个全新的注册表，它接受包含 Lean 代码的 GitHub 仓库快照，检查形式化陈述是否通过类型检查，并使用大语言模型将非形式化描述与声称的结果进行比较。机械检查（使用 Lean 工具 Comparator）保证了逻辑正确性，而 AI 检查则为非形式化陈述提供了非确定性的合理性测试。Palomar 明确不进行关于新颖性或趣味性的真人同行评审，这反映了 arXiv 的最低接受标准。

Submission workflow is intentionally rigorous yet achievable

提交流程设计得既严谨又切实可行：

一个包含简洁、人类可读的定理 Lean 陈述的 challenge file。
一个包含完整 Lean 证明的 solution module。
一个提供非形式化描述、元数据和披露信息的 formalization.yaml 文件。

Tao 成功通过注册他自己的 Sendov 猜想的正式证明展示了这一过程。该注册表接受来自人类、AI agent 或混合模式的贡献，现代 AI 助手可以协助完成提交中的机械性工作。

Community reaction highlights strengths and concerns

"The second check (b) is non‑deterministic, being performed by a large language model. Shouldn’t this be just preliminary? I think submissions should have an additional, human‑performed level of verification." – Anonymous comment

"We do not have the resources to host and maintain repositories directly, but would be open to expanding the whitelist of approved repository hosting services beyond Github if there is sufficient demand for doing so." – Terence Tao

"A very quick look at Palomar suggests that it would be much more helpful if each submission required (a) a meaningful Title, and (b) a (well‑written) Abstract explaining what is proved — just as one sees in arXiv." – David Bevan

"Palomar will definitely be something we integrate for data checks and validation" – ygtisik (author of a registry of AI usage in science).

这些评论突出了三个反复出现的主题：

Verification depth – 一些用户希望在自动化检查之外增加一层人工评审。
Repository hosting – 对 GitHub 的依赖被视为单点故障；扩展到其他托管服务是理想的。
Metadata quality – 更清晰的标题和摘要，可以提高可发现性，类似于 arXiv 的惯例。

Technical design choices and trade‑offs

GitHub‑centric model – 简化了身份验证、垃圾邮件控制和版本控制，但同时也对单一服务产生了依赖。正如几位评论者所指出的，未来的扩展可能会将其他 git forges 加入白名单。
AI‑driven semantic check – 提供了一种可扩展的方式来标记形式化陈述与非形式化描述之间的不匹配，但它仍然是非确定性的。注册表将此视为初步筛选，而非最终判定。
Minimal human involvement – 模仿 arXiv 的方法，允许系统在无需专门评审团队的情况下，扩展到预期的 Lean formalization 的规模。

Why mathematicians might contribute

Visibility – 条目会出现在可搜索的注册表中，为作者提供认可并向更广泛的社区进行展示形式化成果。
Reusability – 经过验证的 Lean 证明可以被导入到其他项目中，从而减少重复劳动。

t* AI ecosystem support – 注册表提供了高质量、机器可检查的数据，这些数据可以用于训练或评估 AI 证明助手。

Community standards – 参与其中有助于塑造 Lean formalization 的的最佳实践惯例。

Comparison with existing efforts

TheoremDB 和 Metamath 已经提供了形式化证明的可搜索数据库，但 Palomar 专注于 Lean，并集成了自动化类型检查以及基于 AI 的语义验证。
Isabelle AFP 为 Isabelle/HOL 提供了一个长期运行的存档库；Palomar 可以被视为 Lean 的对应物，尽管目前仍处于早期阶段。

Outlook and open questions

Human‑level validation – 第三方服务可以在 Palomar 的最低限度检查之上增加同行评审层。
Metadata enhancements – 在 formalization.yaml 中添加显式的标题和摘要字段，将使条目符合学术预印本的标准。
Hosting diversification – 扩展到 GitHub 之外，可以减轻对单一平台的依赖，并适应使用其他 forges 的用户。

Palomar is now open for submissions. Detailed instructions are available at the registry’s how‑to‑submit page, and discussion continues on the dedicated Lean Zulip channel.