It may sound highly unlikely that scientists have proven the existence of God, while their work reflects on things being proven, not believed. However, the Austrian-American mathematician **Kurt Friedrich Gödel** created a theorem using a mathematical equation to prove God’s existence, which was later confirmed by computer scientists to be true.

Before he died, Gödel left behind a provoking theory based on philosophies of modal logic, which was that a higher being must exist.

However, the particulars of the mathematics involved in Gödel’s ontological proof are quite complex. Nevertheless, in principle, he was arguing that, by definition, God is that for which no greater can be conceived. And while God exists in the perception of the notion, we could imagine him as greater if he really existed. Ergo, he must exist.

**The equation was as follows:**

Ax. 1. {P(φ)∧◻∀x[φ(x)→ψ(x)]} →P(ψ)Ax. 2.P(¬φ)↔¬P(φ)Th. 1.P(φ)→◊∃x[φ(x)]Df. 1.G(x)⟺∀φ[P(φ)→φ(x)]Ax. 3.P(G)Th. 2.◊∃xG(x)Df. 2.φ ess x⟺φ(x)∧∀ψ{ψ(x)→◻∀y[φ(y)→ψ(y)]}Ax. 4.P(φ)→◻P(φ)Th. 3.G(x)→G ess xDf. 3.E(x)⟺∀φ[φ ess x→◻∃yφ(y)]Ax. 5.P(E)Th. 4.◻∃xG(x)

* According to Gödel*, a “God-like” being has all positive properties and that the essence of a being is the property the being has, and that property suggests any property of that being.

He also stated that the necessary existence of that being is necessary and that all of that being’s essence exist. Finally, he said that being god-like is the essence of any God-like being.

Thus, Bruno Woltzenlogel Paleo of the Technical University in Vienna and Christoph Benzmüller of Berlin’s Free University were two computer scientists who run Gödel’s equation on a computer and verified it. Nonetheless, according to Paleo and Benzmüller, the main purpose for the research itself was not to actually prove God’s existence but to highlight the power of the program. They were not so interested in proving God’s existence.

Therefore, the program they used had to deal with modal logic that can recognize words such as necessity and possibility. When looking at philosophy, modal logic appoints to proclamations that speak about possibility and necessity, like “if something exists” or “if all this something has this property, then.”

According to the scientists, they used different kinds of modal logic systems to check if Gödel’s proof is actually true. Of course, outcome of the research left them appaled.

Judging from the results of the research, they found that Gödel’s calculations can be proven inevitably in just a few seconds, using a MacBook nontheless.

This goes to show that computers can be used to prove all types of equations and endless possibilities come to mind. Benzmüller and Paleo’s original submission on the arXiv.org research article server is entitled “Formalization, Mechanization and Automation of Gödel’s Proof of God’s Existence.”

*“The fact that formalizing such complicated theorems can be left to computers opens up all kinds of possibilities, Benzmüller told SPIEGEL ONLINE. “It’s totally amazing that from this argument led by Gödel, all this stuff can be proven automatically in a few seconds or even less on a standard notebook,” he said.*

* **“I didn’t know it would create such a huge public interest but (Gödel’s ontological proof) was definitely a better example than something inaccessible in mathematics or artificial intelligence,” the scientist added. *

*“It’s a very small, crisp thing, because we are just dealing with six axioms in a little theorem. … There might be other things that use similar logic. Can we develop computer systems to check each single step and make sure they are now right?”*

To some, this equation and the name, “*Gödel**” *may not mean much, but to scientists he is praised just as much as Albert Einstein, who was in fact, a close friend of Gödel’s. He is still remembered and celebrated for his findings.

However, Gödel’s method is not the only existing one that initiates the proof of existence of God through the use of mathematical equations. Thus, Euclid also employed the same method using axioms and definitions.

He used them to build theorems while utilizing logic at the same time. According to him, the only way to disprove these axioms is to disagree with one or two of them. When you think about it, same thing actually applies to Gödel’s proof, which states that if someone wants to discredit or disqualify him, they must change one or two axioms.

.