" Gödel's ontological proof has been analysed for the first-time with an
unprecedent degree of detail and formality with the help of higher-order
theorem provers. The following has been done (and in this order): A
detailed natural deduction proof. A formalization of the axioms,
definitions and theorems in the TPTP THF syntax. Automatic verification
of the consistency of the axioms and definitions with Nitpick. Automatic
demonstration of the theorems with the provers LEO-II and Satallax. A
step-by-step formalization using the Coq proof assistant. A
formalization using the Isabelle proof assistant, where the theorems
(and some additional lemmata) have been automated with Sledgehammer and
Metis"
