2 ms·

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

Fun fact: the proof is formalised in TPTP (a standard benchmark library for automated theorem provers). It is considered of average difficulty. http://www.tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=PHI&File=PHI003^1.p http://www.tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain...

bcaa7f3a8bbc 7y ago
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)? https://github.com/FormalTheology/GoedelGod https://github.com/FormalTheology/GoedelGod
- andrepd 7y ago
  I believe not. This was the citation given in the problem: https://arxiv.org/abs/1308.4526 https://arxiv.org/abs/1308.4526
  - andrepd 7y ago
    Silly me, we're talking about the same thing :p