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