文章摘要
陶哲轩介绍了Palomar项目，这是一个Lean验证数学的注册表，旨在系统记录和追踪已用Lean证明的数学定理，推动形式化验证在数学领域的应用。
文章总结
近日，陶哲轩宣布，由Lean FRO和ICARM孵化的“Palomar Lean验证数学注册中心”现已开放提交。该中心旨在为Lean语言形式化的数学证明提供一个类似预印本服务器的注册平台，以应对日益增多的AI生成证明带来的验证难题。
Palomar注册的是外部GitHub仓库的快照，这些仓库需包含：一个用Lean语言简洁描述结果的“挑战文件”、一个包含完整证明的“解决方案模块”，以及一个用非正式语言描述结果并附带元数据的“formalization.yaml”文件。提交后，系统会进行两项检查：一是利用Lean工具“Comparator”机械验证解决方案模块是否通过类型检查并准确证明了挑战文件中的结果；二是通过大语言模型非确定性检查非正式描述与挑战文件是否匹配。需强调的是，这并非同行评审，而是确保基本合规。
陶哲轩本人已成功提交了Sendov猜想的证明作为测试，并计划提交更多早期形式化成果。该注册中心欢迎人类生成、AI生成或混合生成的证明提交，但建议提交前进行人工审核。相关讨论将在Zulip频道进行。
评论总结
根据评论内容，总结主要观点如下：
1. 对Palomar项目的积极评价与期待 - 评论认为该项目将数学领域形式化为互联系统，是“数学理解的索引”，并预言所有领域都将经历类似变革（评论2）。 - 关键引用："Turning the entire field of mathematics into a formalized and connected system... All fields will undergo this change!!!"（评论2）
2. 对激励机制与实用性的质疑 - 有评论质疑用户为何愿意贡献内容，缺乏明确激励（评论1）。 - 关键引用："why people would contribute submissions to Palomar. What is the incentive?"（评论1）
3. 技术实现与依赖性问题 - 部分评论批评项目依赖GitHub，认为应支持更通用的版本控制系统（评论8），并指出类似项目（如Isabelle的AFP、Metamath、theoremdb）已存在（评论4、6、9）。 - 关键引用："Either possibility is unfortunate. I do not like GitHub's de-facto mindshare monopoly"（评论8）；"Lean keeps re-inventing everything Isabelle has had for decades"（评论9）
4. 对验证过程与数学本质的反思 - 有评论指出验证证明的递归性问题（评论3），以及手动审核可能无法应对无限琐碎定理的挑战（评论7）。 - 关键引用："you now have to prove your proof that their proof proves their claimed statement"（评论3）；"one might come up with an infinite amount of useless theorems"（评论7）
5. 对作者身份的调侃 - 评论7幽默地指出，作者陶哲轩以“连我都能做到”鼓励他人，但忽略其作为顶尖数学家的特殊性。 - 关键引用："he almost makes it sounds like 'If even I can do it, you can too!'"（评论7）