Palomar——Lean 验证数学注册中心

摘要

陶哲轩近日宣布，Palomar——一个由 Lean FRO 和 ICARM 孵化的 Lean 验证数学注册中心现已开放提交。该中心旨在作为 Lean 证明的预印本服务器，接受包含挑战文件、解决方案模块和 formalization.yaml 的 GitHub 仓库快照。提交后，系统将检查解决方案模块是否类型检查并通过挑战文件中的声明，以及非正式描述是否与正式声明匹配。陶哲轩担任科学顾问委员会成员。这一举措旨在应对 AI 生成的 Lean 证明日益增多但验证困难的问题。