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 auto
arXiv cs.AIResearch source·