Gödel's ontological proof & Benzmüller's work 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 ?
 A: Gödel’s proof has the nice feature that one can cleanly separate the logical core of the argument (which is uncontroversial—but see the next paragraph) from its alleged application to theology (which of course is going to be controversial).  My opinion is that the main significance of Gödel’s proof is that it shows that there is something to the ontological argument; many people (including my teenage self), when first encountering the ontological argument, perceive it to be total nonsense.  Immanuel Kant’s “existence is not a predicate” objection was taken by many to be a decisive refutation.  So showing that the ontological argument isn’t completely free of content is already a significant intellectual achievement.
The work of Benzmüller (and Paleo) is interesting because it showed that a (fixable) mistake in Gödel’s proof was more serious than people had previously realized.  See The Inconsistency in Gödel’s Ontological Argument: A Success Story for AI in Metaphysics for more details.
A: I know Benzmüller's work from a slightly different context, formalizing other interesting systems of modal logic. Hadn't heard of this specific project, but it seems very admirable.

*

*Formalization of proofs is a highly respectable activity

*Any "proof of existence of God" written by Gödel is bound to inspire curiosity and interest in logic among the public, thus contributing to education

