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. I recently posted a [preprint][1], which was highlighted by the cover of the French magazine [Science et Vie][2].

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 ?


  [1]: https://www.researchgate.net/publication/342159229_A_Simplified_Supreme_Being_Necessarily_Exists_says_the_Computer_Computationally_Explored_Variants_of_Godel%27s_Ontological_Argument
  [2]: https://www.science-et-vie.com/archives/pourquoi-on-croit-en-dieu-les-mathematiques-ont-enfin-la-reponse-57595