The famous logician Kurt Goedel left behind a formalized "proof" for the ontological argument of Anselm of Canterbury.

Anselm gave a "proof" that the term "a being than which none greater can be conceived" must refer to some existing being, i.e., that there must exist a being than which none greater can be conceived.

See the following lecture by tje logician Brendel for a formalization of Goedels "proof"

http://wwwmath.uni-muenster.de/logik/Veranstaltungen/cl2010/slides/brendel.pdf

It closes with a critical assessment of what Goedel's formalization prove and what it does not prove.