For a decade or so, Christoph Benzmüller from Berlin has explored Gödel's ontological proof (and variants) of existence of God. He uses the proof assistant Isabelle/HOL. He recently posted a preprint, which was highlighted by the cover of the French magazine Science et Vie.

Well, I am not familiar with AI, yet even less with applications to metaphysics. But many practitioners of MO must be. I should like to know how serious is Benzmüller's work considered in this community. Is it controversial or is this considered a respectable research activity ?