发表机构
Otto-Friedrich-Universität Bamberg; Freie Universität Berlin（班贝格奥托·弗里德里希大学; 柏林自由大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
将 Gödel 与 Scott 的本体论论证的 Isabelle/HOL 形式化完整移植到 Lean 4，重新证明所有结果，并利用 Lean 4 特性给出所需模态逻辑的上界。
AI 中文摘要
本文介绍了将 Benzmüller 和 Scott 关于 Gödel 模态本体论论证及其 Scott 变体的 Isabelle/HOL 数据集完整、保持结构地移植到 Lean 4 的工作。该移植包含 30 个 Lean 4 模块，对应每个 Isabelle/HOL 理论，保留了节结构、声明顺序以及每个公理、定义、引理和定理的名称；一个比较工具认证了所有 548 条语句完全相同。Isabelle/HOL 开发中证明的所有内容均被重新证明，包括 Gödel 1970 年公理的不一致性、修复后的 Gödel 变体、Scott 变体、模态坍缩、一神论以及正属性的超滤子性质；原始开发中在自动化证明器找到证明后未重放的五条语句（其中一条随后被假定）也被证明。剩余的 45 条未证明语句恰好是原始开发中通过 nitpick 反驳（35 条）或留作开放（10 条）的语句；它们是匿名的 sorry，且没有其他语句依赖于它们。Lean 4 的两个特性影响了这一结果。它既没有 sledgehammer 也没有模型查找器，因此单行自动化证明变成了显式的证明项，72 次 nitpick 调用被记录为文档。此外，#print axioms 报告了每个证明所消耗的公设，为每个结果提供了其所需模态逻辑的上界：Scott 的必然存在定理和模态坍缩仅需可达关系的对称性（逻辑 KB）；本质引理、一神论引理以及类神存在的可能性不需要框架条件（后者仅有一个例外，即原始记录中的混合量词设置）；而 Gödel 1970 年公理的不一致性也不需要任何框架条件。该开发不依赖 Lean 4 核心之外的任何库；源代码、比较工具和两个 Isabelle 交叉检查会话作为辅助文件包含在内。
英文摘要
The Isabelle/HOL dataset of Benzmüller and Scott's study of Gödel's ontological argument and Scott's variant (Monatshefte für Mathematik, 2025) is carried to Lean 4 and from there back to the automated provers, as a benchmark independent of either proof assistant. The port covers all thirty theories, structure and names preserved: 548 statements compare identical as parsed, every named result is proved again, and five results the original reports without replaying them are proved here. For every theorem, #print axioms gives the postulates its proof consumes: Scott's necessary existence and modal collapse need only a symmetric frame, confirming that KB suffices. The benchmark, in TPTP THF and SMT-LIB, turns the steps of an argument debated in philosophy into 294 theorems, alongside 45 statements the original refutes or leaves open, ten left open there. Five THF provers, and cvc5 on SMT-LIB, prove 227 theorems within ten seconds on one core and 232 within sixty, and none proves any of the 45. E and Leo-II solve the most, although Leo-II's calculus has been unchanged for about a decade and was only repaired and modernised here, as release 2.2. Vampire, whose later version won the higher-order division of CASC-30, solves the most in no configuration. Only E and Leo-II are measured in their own automatic mode: Zipperposition proves 101 in a single mode and 213 with its developers' portfolio, Vampire 174 without options and 209 with a higher-order schedule that its CASC mode does not select, and Leo-III 159 alone and 177 with E as partner.
Comments57 pages. Version 3 measures every prover in the setting it is used in (CASC, SystemOnTPTP, Sledgehammer), which changes several figures, and cites the companion article arXiv:2609.36279, which settles all ten statements the dataset leaves open. Ancillary files: the Lean 4 package, its typeset sources, the tools, and both renderings with every prover result
