本文介绍了将 Isabelle/HOL 数据集完整迁移到 Lean 4 的工作。迁移保持了原始 30 个 Isabelle/HOL 理论对应的 30 个 Lean 4 模块，保留章节结构、声明顺序以及每个公理、定义、引理和定理的名称。比较工具验证了全部 548 条陈述在两套系统中完全一致。所有 Isabelle/HOL 证明的结果在 Lean 4 中重新证明，包括 Gödel 1970 公理的不一致性、修正后的 Gödel 变体、Scott 变体、模态坍缩、一神论以及正属性的超滤子性质。原始工作中因自动定理 prover 找到证明但未手工复现的 5 条语句也在本移植中得到证明；其余 45 条未证明的语句正好对应原始使用 nitpick 反例或留下悬而未决的情况，它们在 Lean 4 中表现为匿名 sorry，且没有其他结果依赖它们。
Lean 4 的两个特性影响了移植方式：没有 sledgehammer 也没有模型查找器，使得原来的一行自动证明必须展开为显式的 proof term；72 次 nitpick 调用被记录为文档。使用 #print axioms 可以看到每个证明依赖的公理，从而得到所需模态逻辑的上界。例如，Scott 必要存在定理和模态坍缩只需要可达关系的对称性（KB 逻辑），而本质性、单一神论以及上帝般存在的可能性不需要任何框架条件，Gödel 1970 公理的不一致性同样不依赖框架。
整个开发仅依赖 Lean 4 核心库，无需额外库。源码、比较工具以及两次 Isabelle 交叉检查会话均作为附属文件提供。
点评