陶哲轩推出Palomar：Lean验证数学注册库

Palomar: A registry of Lean verified mathematics

近期，AI生成的数学证明在Lean证明助手中大量涌现，但验证这些证明是否真实有效却非易事。为了解决这一混乱，我宣布由Lean FRO和ICARM孵化的Palomar注册库正式开放提交。Palomar类似于Lean证明的预印本服务器，它收录符合最佳实践的GitHub仓库快照，要求包含挑战文件、解决方案模块以及描述结果的formalization.yaml文件。系统将通过Comparator工具进行机械检查，并利用大语言模型验证非形式化描述的一致性。值得注意的是，Palomar并非同行评审期刊，而是旨在为新旧结果（无论是人类还是AI生成）提供一个透明的注册平台。我已成功将Sendov猜想证明的正式化版本提交至该库。