Hacker News Reader

Fun fact: the proof is formalised in TPTP (a standard benchmark library for automated theorem provers). It is considered of average difficulty.

Is it related to the GoedelGod project (which was an open source project on attempting to formalize Godel's Ontological Proof, was in GSoC 2017)?

I believe not. This was the citation given in the problem: https://arxiv.org/abs/1308.4526

Silly me, we're talking about the same thing :p