The consistency of the basic assumptions made by Gödel was confirmed by the computer. Furthermore, the scientists were able to demonstrate that the nontrivial proof was, for the most part, able to be generated automatically by the computer. They had not expected that to be the case. This means that in addition to using such systems to prove theorems in philosophy and mathematics, in the future they could be used in dialogue systems so that computers can be used to understand human reasoning patterns and even augment them.

The logic formalism used by Gödel – a so-called higher-order modal logic that uses terms like "necessary" and "possible" – was previously thought to be too complex and difficult to represent and automate on the computer. Available theorem provers are mainly based on much simpler formalisms. To circumvent this problem, the researchers used a methodology that allowed them to automate Gödel's higher-order modal logic using existing theorem provers. This trick is based in turn on the theoretical work of Benzmüller and Paulson from the University of Cambridge. For the classical higher-order logic, several theorem provers were developed in the last two decades. They were now successfully used in the work by Benzmüller and Woltzenlogel Paleo, including a theorem prover developed by Benzmüller.

Kurt Gödel's mathematical proof of God was published after his death. It belongs to the class of so-called ontological proofs, which have a long tradition in philosophy. As constructions of pure thought, they were previously and are still, hotly debated in the scientific world. In an ontological proof of God, the existence of God is deduced from a few abstract axioms and definitions through a logical progression. Conversely, one can say that God's existence is reduced to the validity of these axioms and definitions.

A number of well-known philosophers including St. Anselm, Descartes, Leibniz, and Kant, have dealt intensively with ontological proofs of God. Two issues are relevant for this type of proof: (A) Are the chosen assumptions valid and useful? (B) Is the logical chain of reasoning actually correct? Dealing with issue (A) is up to the fields of philosophy and theology, and ontological proofs of God have in the past often, and justifiably so, been criticized on this point. Dealing with issue (B) is a matter of mathematical and philosophical logic. The logic formalism used in Gödel's proof is not trivial. Up to now analysis of the logical aspects was done exclusively with paper and pencil, which is both tedious and prone to error.

Benzmüller and Woltzenlogel Paleo now want to investigate Gödel's proof further and thereby also respond to recent work that criticizes the deeper logical aspects of Gödel's work. They also plan to use their method to check other ontological proofs of God for their logical validity. Logic formalism and assumptions may then be regarded as variable parameters. Using these parameters the researchers aim to experiment with the theorem prover to gain new insights into the logical structure of the arguments. According to the researchers, this would yield interesting perspectives for a computer-assisted theoretical philosophy and metaphysics. They expect to be able to effectively and flexibly check the validity of conclusions based on assumptions.

The age-old question of God's existence of course remains unanswered and depends on the meaningfulness and reference to reality of the chosen axioms. Gödel's reasoning, however, in the opinion of the computer scientists has been proven to be correct, as demonstrated by the computer.

A translation of Gödel's proof sketch (in the version of Gödel's student Dana Scott) from formal logic into natural language:

• Axiom 1: Either a property or its negation is positive.
• Axiom 2: A property that is necessarily implied by a positive property is positive.
• Theorem 1: Positive characteristics may be due to an existent entity.
• Definition 1: A God-like entity has all the positive features.
• Axiom 3: The property of being God-like is positive.
• Conclusion: Perhaps God exists.
• Axiom 4: Positive characteristics are necessarily positive.
• Definition 2: A property is the essence of an entity, if it belongs to the entity and necessarily implies all the properties of the entity.
• Theorem 2: To be God-like is the essence of every God-like entity.
• Definition 3: An entity exists necessarily if all of its essences are necessarily realized in an existing entity.
• Axiom 5: Necessarily existing is a positive property.
• Theorem 3: God must necessarily exist.