机器写的证明多到数学家专门建了一个登记处——而它的两道检查里，有一道是由语言模型完成的

陶哲轩于 8 月 18 日宣布，由 Lean FRO 与 ICARM 孵化的 Lean 验证数学登记库 Palomar 已开放投稿。它要解决的问题很新：过去几个月里，针对新旧结果的 AI 生成证明大量涌现，其中相当一部分已在 Lean 中形式化——这是一个能让机器逐步核验的证明助手。但 GitHub 上摆着的一个 Lean 仓库并不会自我解释。要弄清代码是否真的证明了作者所声称的东西，是一件实打实的苦活，对不使用 Lean 的数学家来说几乎不可能。Palomar 让提交的仓库通过两道检查。第一道是机械的：名为 Comparator 的 Lean 工具确认该模块通过类型检查，并且恰好证明了所声称的结果。第二道则追问自然语言描述是否与形式化陈述相符，而这一道由一个大语言模型完成。两道都通过的仓库会被登记，同时公布确切陈述、所依赖的库以及审阅意见。陶哲轩称之为 Lean 证明版的预印本服务器，并与 Jeremy Avigad、Matthew Ballard、Jaume de Dios、Nestor Guillen、Bryna Kra、Kim Morrison、Ravi Vakil 和 Akshay Venkatesh 一同担任科学顾问委员会成员。

✓ 已核实 · 4个来源

相关新闻