Palomar——Lean验证数学注册表
内容提要
陶哲轩宣布Palomar数学验证注册表开放提交，旨在验证Lean证明的可靠性。该注册表由Lean FRO和ICARM孵化，检查代码是否通过类型检查、无额外公理，且形式化陈述与描述匹配。提交需通过机械检查和AI模型验证，但非同行评审。陶哲轩已成功提交Sendov猜想证明，欢迎新旧结果及AI辅助提交。
延伸解读
Palomar的定位与局限
Palomar被描述为Lean证明的预印本服务器，而非同行评审期刊。其检查分为机械验证和AI模型验证，但明确强调这远不及人类同行评审对新颖性、趣味性和准确性的审查。因此，注册结果应视为初步验证，而非最终认可。
提交的实际门槛
提交过程虽详细但可行，陶哲轩本人成功提交了Sendov猜想的证明。提交需满足技术要求和格式规范，包括类型检查、无额外公理、形式化陈述与描述匹配。AI工具可辅助处理机械细节，但人工审查仍被强烈建议，表明完全依赖AI提交可能仍有风险。
对AI生成证明的意义
随着AI生成证明的增多，Palomar提供了一种标准化验证途径，有助于区分可靠与不可靠的证明。它欢迎新旧结果及AI辅助提交，但需注意其验证标准并非绝对，可能无法捕捉所有错误。因此，读者在依赖这些结果时仍需保持谨慎。
Q&A
Palomar是什么？
Palomar是一个Lean验证数学注册表，由Lean FRO和ICARM孵化，旨在验证Lean证明的可靠性。它类似于Lean证明的预印本服务器，注册外部GitHub仓库的快照，并检查其是否通过类型检查、无额外公理，且形式化陈述与描述匹配。
Palomar注册表如何验证Lean证明？
Palomar通过两个检查验证Lean证明：一是机械检查，使用Lean工具Comparator确保代码类型检查并证明挑战文件中的结果；二是非确定性检查，由大型语言模型评估非正式描述是否与形式化陈述匹配。
Palomar的验证是否等同于同行评审？
不等同。Palomar的检查（机械检查和LLM检查）远不及人类同行评审对新颖性、趣味性和准确性的全面评估。Palomar不是同行评审期刊。
谁可以提交到Palomar？
任何人都可以提交，无论是人类生成、AI生成还是混合生成的证明。提交需遵循详细说明，并建议进行人工审查。
陶哲轩是否成功提交过证明到Palomar？
是的，陶哲轩成功提交了他对Sendov猜想的证明，并计划提交一些更早的形式化证明。
Palomar注册表由谁孵化？
Palomar由Lean FRO和ICARM孵化。
