Algorithmen kontrollieren immer mehr, aber wer kontrolliert eigentlich die Algorithmen? Einen eher harmlosen⁽¹⁾ Aspekt dieses Themas diskutiert seit einigen Tagen die Frage- und Antwortseite mathoverflow: Proof assistent, cura te ipsum^{2 (1)} nicht nur weil Beweisassistenten im Alltagsgeschäft der Mathematik noch keine große Rolle spielen ⁽²⁾ dtsch.: "Beweisassistent, heile dich selbst" Die Frage ist, wie man automatische Theorembeweiser gegen das irrtümliche Beweisen falscher Theoreme absichern kann; befriedigende Antworten scheint es bisher nicht zu geben. Eine andere, komplementäre Frage, die bei mathoverflow auch gerade diskutiert wird, betrifft Proofs shown to be wrong after formalization with proof assistant. Zwar sind die meisten bisher mit automatischen Theorembeweisern überprüften Lehrsätze eher klassische Sätze, deren Beweise schon Tausende Male von Mathematikern gelesen und verstanden wurden und wo man schon deswegen keine versteckten Fehler mehr finden wird. Aber es wurde jedenfalls bei der Computerüberprüfung des Beweises der Keplerschen Vermutung ein (korrigierbarer) Fehler gefunden und es gibt in den Antworten der mathoverflow-Frage den Bericht eines an computer-formalisierten Beweisen arbeitenden Doktoranden, der in anonymisierter Form von den zahlreichen Fehlern berichtet, die er dank seiner Arbeit in Lehrbüchern und Veröffentlichungen findet. (Eine kuriose Geschichte in dem Zusammenhang: in einem von Kurt Gödel in seinen späten Jahren veröffentlichten Gottesbeweis fand 2013 ein automatischer Theorembeweiser eine bis dahin übersehene Inkonsistenz: The inconsistency in Gödel‘s ontological argument: a success story for AI in metaphysics.) Jedenfalls scheint es einfacher zu sein, mit Computern Fehler in menschlichen Arbeiten zu finden, als Computer dazu zu bringen, Fehler in ihren eigenen Algorithmen aufzuspüren.

Um einen Kommentar zu verfassen, müssen Sie sich einloggen bzw. kurz als Gast registrieren.