Palomar：精益验证数学的注册表

近几个月来，人工智能生成的各种新旧结果的证明激增，其中一些已用证明辅助语言 Lean 形式化。然而，检查给定的精益存储库实际上证明所声明的声明有些不简单，特别是对于不擅长使用精益的读者来说：必须首先检查所声明的正式精益声明是否具有类型检查的证明，证明不包含任何“作弊”，例如添加额外的公理，并且正式声明也与所声明结果的非正式描述相匹配（在语义意义上）。为了帮助澄清这一情况，我很高兴地宣布，Palomar 精益验证数学注册表现已开放接受提交，该注册表是由 Lean FRO 和 ICARM 孵化的一项计划。我在该登记处担任多个职务，包括与 Jeremy Avigad、Matthew Ballard、Jaume de Dios、Nestor Guillen、Bryna Kra、Kim Morrison、Ravi Vakil 和 Akshay Venkatesh 一起担任科学顾问委员会成员。可以在此处找到 Palomar 的详细动机，也可以在此处找到有关 Palomar 的更多信息。 Palomar 的零级近似是精益校样的预印本服务器。更准确地说，Palomar（以天文台命名）是外部 Github 存储库（或更准确地说，此类存储库的“快照”，由特定的 Github 提交表示）的注册表，其中包含遵循此类形式化的当前最佳实践的精益代码，特别是包含一个“挑战文件”，其中包含对声称的结果的简短的、人类可读的精益描述。一个“解决方案模块”，包含挑战文件中声明的结果的（任意长的）证明。 “formalization.yaml”文件以非正式语言描述结果，还包含许多其他相关元数据和披露信息。 （存储库还有一些额外的技术要求，我将在此处省略。）如果将存储库的快照提交给 Palomar，它将检查 (a) 解决方案模块是否进行类型检查并准确证明挑战文件中声明的结果，以及 (b)formalization.yaml 文件中结果的非正式描述是否与挑战文件中声明的结果匹配，以及存储库是否满足注册表项所需的各种最低标准。第一个检查 (a) 是纯机械的，使用精益工具比较器；第二个检查 (b) 是不确定的，由大型语言模型执行。如果存储库通过了两项检查，则可以在 Palomar 上注册。值得强调的是，(a) 和 (b) 中的检查远远低于对提交的新颖性、兴趣和准确性进行适当的人类同行评审所得到的结果；特别是，Palomar 不是同行评审期刊。提交过程是彻底的，但是是可以实现的：作为测试，我成功地将我自己最近的 Sendov 猜想证明的形式化提交给 Palomar，并计划很快向注册表提交一些较旧的形式化。无论如何，登记处现在已经开放，可以正式确定旧结果和新结果。欢迎提交（无论是人类生成的、人工智能生成的还是两者的混合）；请在开始提交之前阅读此处的（有些详细的）说明。 （不过，我要指出的是，现代人工智能代理在协助处理提交的机械细节方面非常有帮助，尽管仍然强烈建议进行人工审核。）有关 Palomar 的讨论和反馈将在此 Zulip 频道上进行。