Palomar：Lean 形式化数学证明注册平台上线

近几个月来，人工智能生成的各种旧和新结果证明大量涌现，其中一些已被形式化成证明助手语言Lean。然而，要检查某个精益仓库是否真的证明了所声称的陈述，对于不熟悉精益的受众来说，这并不简单：首先必须检查所声称的形式精益陈述是否存在类型校验的证明，证明中是否包含任何“作弊”，比如添加额外公理。 并且这些正式陈述在语义上也与声称结果的非正式描述相符。

为了让情况更清晰，我很高兴地宣布帕洛玛精益验证数学注册库，这是由精益 FRO以及ICARM现已开放投稿。我在该登记册中担任多个职务，包括科学顾问委员会成员，杰里米·阿维加德,马修·巴拉德,豪梅·德·迪奥斯,内斯特·吉伦,布莱娜·克拉,金·莫里森,拉维·瓦基尔， 和阿克谢·文卡特什.

关于帕洛玛的详细动机可以找到给你，以及关于帕洛玛的更多信息都可以找到给你.Palomar 意图的零近似是精益证明的预印本服务器。更准确地说，是帕洛玛（以天文台）是一个外部 Github 仓库的注册表（更准确地说，是这些仓库的“快照”，由特定的 Github 提交表示），包含遵循当前此类形式化最佳实践的精益代码，特别是包含

• 一个“挑战文件”，包含简短、易读的精益描述，描述所声称的结果。
• 一个“解答模块”，包含挑战文件中声称结果的（任意长的）证明。
• A “formalization.yaml文件中以非正式语言描述了结果，同时还包含许多其他相关的元数据和披露内容。

（仓库还有一些额外的技术要求，我这里略去。）如果向 Palomar 提交仓库快照，它会检查 （a） 解决方案模块是否对类型校验并证明了挑战文件中声称的结果，以及 （b） formalization.yaml 文件中对结果的非正式描述是否与挑战文件中声称的结果相符，并且该仓库是否满足注册表条目的各种最低标准。

第一个检查（a）纯机械，使用精益工具比较器;第二个检查（B）是非确定性的，由大型语言模型执行。如果仓库通过了这两个检查，就可以在Palomar上注册。

值得强调的是，（a）和（b）中的检查远远达不到对提交内容进行适当人工同行评审以评估新颖性、趣味性和准确性所能提供的水平;特别是，帕洛玛是不是一份同行评审期刊。

提交过程很严格，但可以实现：作为测试，我成功管理提交我自己的森多夫猜想证明的最新形式化并计划很快向登记处提交一些较早的正式申请。

无论如何，该登记处现已开放，供新旧结果的正式化。欢迎投稿（无论是人生成、AI生成，还是两者混合）;请阅读（较详细的）说明给你在开始投稿之前。

（不过我要指出，现代AI代理在协助提交的机械细节方面非常有帮助，尽管仍然强烈建议人工审核。）

关于帕洛玛的讨论和反馈将会在这个祖利普频道.