# Formalization, Mechanization and Automation of G"odel's Proof of God's Existence

arXiv: https://arxiv.org/abs/1308.4526 · HTML: https://mlsanity.com/paper/1308.4526/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 21 Aug 2013.

## Built on by (most cited first, 5 of 5)

- [TPTP World Infrastructure for Non-classical Logics](https://mlsanity.com/paper/2508.09318/) (2025)
- [G"odel's and Scott's Variants of the Ontological Argument in Lean 4 and TPTP THF](https://mlsanity.com/paper/2609.26806/) (2026)
- [Applying Second-Order Quantifier Elimination in Inspecting G"odel's Ontological Proof](https://mlsanity.com/paper/2110.11108/) (2021)
- [A Simplified Variant of G"odel's Ontological Argument](https://mlsanity.com/paper/2202.06264/) (2022)
- [Proofs Without Nominals: G"odel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes](https://mlsanity.com/paper/2609.36279/) (2026)

## Abstract (arXiv)

G"odel'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.