nitpick

Gödel's Ontological Argument Ported to Lean 4

研究人员已成功将关于 Gödel 和 Scott 的本体论论证的数据集从 Isabelle/HOL 移植到 Lean 4 编程语言。此次全面的移植保留了原始结构，包括 30 个模块和声明顺序，并使用比较工具验证了 548 个声明的相同性。该项目重新证明了原始研究的所有结果，例如 Gödel 1970 年公理的不一致性以及模态崩溃的概念，并解决了先前被反驳或未解决的声明。