陶哲轩推出Palomar：Lean验证数学注册库
Palomar: A registry of Lean verified mathematics
近期，AI生成的数学证明在Lean证明助手中大量涌现，但验证这些证明是否真实有效却非易事。为了解决这一混乱，我宣布由Lean FRO和ICARM孵化的Palomar注册库正式开放提交。Palomar类似于Lean证明的预印本服务器，它收录符合最佳实践的GitHub仓库快照，要求包含挑战文件、解决方案模块以及描述结果的formalization.yaml文件。系统将通过Comparator工具进行机械检查，并利用大语言模型验证非形式化描述的一致性。值得注意的是，Palomar并非同行评审期刊，而是旨在为新旧结果（无论是人类还是AI生成）提供一个透明的注册平台。我已成功将Sendov猜想证明的正式化版本提交至该库。
Palomar的初衷是成为Lean证明的预印本服务器。
HN 评论区
39- JuniperMesos
Palomar 的零阶近似可以理解为 Lean 证明的预印本服务器。更准确地说，Palomar（以天文台命名）是一个外部 Github 仓库（或更确切地说是由特定 Github commit 代表的仓库“快照”）的注册库，其中包含遵循当前最佳实践的 Lean 代码。
要么 Terry Tao 不精确且不准确地将流行的 Git 仓库托管服务“Github”当作开源版本控制系统“git”的同义词，可能是因为他对软件版本控制有一定了解，但自己并非计算机编程专家；要么他完全理解二者的区别，而 Palomar 的设计确实只针对托管在 GitHub 上的 git 仓库，那么 Tao 的描述就是准确的。无论哪种情况都令人遗憾。我不喜欢 GitHub 在去中心化版本控制系统托管领域的事实垄断地位。
- sva_
提交流程虽然严谨，但完全可以实现：作为测试，我成功提交了自己最近的形式化成果 [...]。
我觉得这种语气很讨喜，他几乎让人感觉像是在说：“连我都能做到，你也一定行！”，尽管他可能是在世的最多产的数学家。
几年前我曾提议，建立一个形式可验证数学证明的区块链会很有意思，但很快就被人们以哥德尔不完备定理为由否决，称这是毫无意义的尝试。
我认为，计算生成数学证明库的一个更大问题在于，人们可能会提出无限多毫无用处且极易证明的定理，不过我想这个注册库是经过人工审核的。数学中存在强烈的归纳偏置，即人类仍然决定哪些公理系统、定理、定义等对我们来说是有意义的。
但我认为，将数年生命投入到证明事物上的这种证明方式，很快将会过时。
- cbondurant
看来 Lean 一直在以更糟糕的方式重新发明 Isabelle 几十年来已有的东西（https://isa-afp.org/）。完全没有理由非要依赖 GitHub。