G\"odel's and Scott's Variants of the Ontological Argument in Lean 4 and TPTP THF

תקציר מקורי באנגליתarXiv:2609.26806v3 Announce Type: replace-cross Abstract: The Isabelle/HOL dataset of Benzm\"uller and Scott's study of G\"odel's ontological argument and Scott's variant (Monatshefte f\"ur 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 argu