This paper presents a complete, structure-preserving port to Lean 4 of the Isabelle/HOL dataset accompanying Benzmüller and Scott's study of Gödel's modal ontological argument and Scott's variant of it. The port comprises 30 Lean 4 modules, one per Isabelle/HOL theory, retaining the section structure, the declaration order and the name of every axiom, definition, lemma and theorem; a comparison tool certifies all 548 statements identical. Everything the Isabelle/HOL development proves is proved again, including the inconsistency of Gödel's 1970 axioms, the repaired Gödel variants, Scott's variant, modal collapse, monotheism and the ultrafilter property of the positive properties; five statements the original leaves unreplayed after an automated prover had found a proof, one of which it then postulates, are proved as well. The 45 remaining unproved statements are exactly those the original refutes by nitpick (35) or leaves open (10); they are anonymous sorrys on which nothing depends. Two features of Lean 4 shape the result. It has neither a sledgehammer nor a model finder, so the one-line automated proofs become explicit proof terms and the 72 nitpick invocations are recorded as documentation. And #print axioms reports the postulates each proof consumes, giving for every result an upper bound on the modal logic it requires: Scott's necessary-existence theorem and modal collapse need only symmetry of the accessibility relation (logic KB); the essence and monotheism lemmas and the possible existence of a God-like being need no frame condition (the latter with the one exception the original records, the mixed-quantifier setting); and the inconsistency of Gödel's 1970 axioms needs none either. The development depends on no library beyond Lean 4's core; sources, comparison tools and two Isabelle cross-check sessions are included as ancillary files.

翻译：暂无翻译