Vor kurzem stieß ich im Internet auf einen Artikel mit der Überschrift: "Computer beweist die Existenz Gottes". Man muss kein Atheist sein, um bei dieser Aussage misstrauisch zu werden und zu seufzen:  "O, Gott, schon wieder so ein Unsinn - und natürlich darf heutzutage der Computer bei so etwas nicht fehlen."   Ein Blick auf die Zusammenfassung belehrte mich aber schon eines besseren,  da hieß es: "Wissenschaftler aus Berlin und Wien haben Kurt Gödels  berühmten Gottesbeweis mit dem Computerprogramm bestätigt". Es wurde mir nun klar, dass hier mit "Beweis" eine Beweisführung gemeint war und in der Tat ging es um automatische Beweise von Theoremen in der Mathematik, allgemeiner um computerunterstützte Beweise in formalen Sprachen.  Als Demonstration für diese Technik, auch "Automatisches Theorembeweisen" genannt, hatten sich zwei Logiker nun den Gödelschen Gottesbeweis herausgesucht.