My friend and colleague George Constantinides wrote an interesting post on his blog recently where he formalises St Anselm’s argument for the existence of God. Since I’m teaching a course on the Isabelle proof assistant this term, I thought I’d see if I could recreate that argument using Isabelle. Here goes… As can be seen… Continue reading Proving the existence of God using a computer→
