# He was correct after all, Gödel’s Proof for the existence of God

Kurt Gödel is considered the greatest logician since Aristotle. Prior to his death, Gödel wrote a proof for the existence of God. Some theorise that the reason he did not publish nor share this proof earlier was for fear of being ostracised by the academic community where he belonged. He was afraid it wouldn’t be cool.

Using a MacBook and proof assistants (Coq and Isabelle), Christoph Benzmüller of Free University of Berlin and Bruno Woltzenlogel Paleo of Free University of Vienna, confirmed that Gödel’s proof was correct, at least as far as higher order model logic is concerned. We might note that KG’s proof indeed, involved modal operators. It only took a few minutes (even seconds) for the computer to validate that the steps KG made in his proof were valid and correct.

Christop and Bruno’s paper can be found here. While the report from Spiegel Online can be found here.