I found a German interview (here) with Prof. Dr. C. BENZMÜLLER. Together with B. WOLTZENLOGEL PALEO he formalized GOEDEL’s proof of God’s existence. The article (in English) here. The two scholars solved a pretty tricky problem of the formalized logic and found ways to express formally difficult logical Annahmen höherer Ordnung using höherstufige Quantoren (Ger., Eng.).
I like the fact that they used Sledgehammer, but not MaSH, or Judgement Day.
[Insert sting / rimshot here]