This paper presents a full, structure‑preserving port of the Isabelle/HOL dataset used in Benzmüller and Scott’s study of Gödel’s modal ontological argument and Scott’s variant to Lean 4. The port consists of 30 Lean 4 modules, one for each Isabelle/HOL theory, preserving the original section hierarchy, declaration order, and the names of every axiom, definition, lemma and theorem. A comparison tool confirms that all 548 statements are identical between the two developments. Every result proved in Isabelle/HOL is reproved in Lean 4, 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 positive properties. The five statements that the original left un‑replayed after an automated prover found a proof (one of which was later postulated) are also proved here; the remaining 45 unproved statements correspond exactly to those the original refuted with nitpick (35) or left open (10) and appear as anonymous sorrys on which nothing depends.
Lean 4’s lack of a sledgehammer‑style prover and of a model finder forces the one‑line automated proofs to be written out as explicit proof terms, and the 72 nitpick invocations are kept as documentation. The command #print axioms reports the axioms each proof consumes, giving an upper bound on the modal logic required: 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 matches the original mixed‑quantifier setting); and the inconsistency of Gödel’s 1970 axioms needs none either.
The development depends only on Lean 4’s core library; source files, the comparison tool, and two Isabelle cross‑check sessions are provided as ancillary material.
Review