Wenn es um höhere mathematische Beweisführung geht, bin ich zugegebener Maßen weit außerhalb meiner sicheren Schwimmtiefe. Darum habe ich erst mal gezögert, mich zu der Meldung zur Bestätigung von Gödels ontologischem Gottesbeweis zu äußern.
Andererseits ist es zwar eine Sache, mathematische Beweise zu führen – eine ganz andere aber, deren Annahmen und Resultate auf ihre Plausibilität zu prüfen. Da genügt manchmal schon eine ziemlich normale Argumentationsfähigkeit.
Ich habe mir also mal das Paper Formalization, Mechanization and Automation of Gödel’s Proof of God’s Existence von Christoph Benzmüller und Bruno Woltenzlogel Paleo angeschaut.
Und nein, ich maße mir nicht an, auch nur eine einzige Zeile in dem zwei Seiten langen Paper anzuzweifeln – ich bin mir sogar absolut sicher, dass die beiden Wissenschaftler (und vor allem ihr Computer, der – wie ich dem Hinweis auf “our computer-assisted formalizations” entnehme – einen Großteil der Arbeit erledigt hat) ganz korrekt vorgegangen sind.
Doch die Existenz Gottes ist damit natürlich nicht bewiesen.