• Deutschlandfunk bei Facebook
  • Deutschlandfunk bei Twitter
  • Deutschlandfunk bei Google+
  • Deutschlandfunk bei Instagram

 
 
Seit 20:00 Uhr Nachrichten
StartseiteForschung aktuellDie Objektivität der Maschine 01.04.2015

Computer als mathematische Gutachter Die Objektivität der Maschine

Der sogenannte Peer-Review-Prozess, das etablierte Gutachterverfahren zur Überprüfung mathematischer Forschungsergebnisse, stößt in manchen Disziplinen an seine Grenzen. Computer könnten aber dafür sorgen, dass es gar keinen Grund mehr gibt, an der Korrektheit zu zweifeln.

Von Thomas Reintjes

Auf einem Computermonitor ist der Binärcode zu sehen. (picture alliance / dpa / Oliver Berg)
Forscher glauben daran, dass Computer irgendwann sogar selbst neue mathematische Felder erschließen können. (picture alliance / dpa / Oliver Berg)

Im englischsprachigen Online-Lexikon Wikipedia gibt es eine Liste langer mathematischer Beweise, die belegt, dass die Mathematik immer komplizierter wird. In den vergangenen 10, 15 Jahren hat demnach die Zahl jener Beweise deutlich zugenommen, die mehrere hundert oder sogar mehrere tausend Seiten umfassen. Kein Mensch kann solche Argumentationsketten noch nachvollziehen oder verstehen. Doch damit sie publiziert und wissenschaftlich anerkannt werden können, müssen Menschen sie im Peer-Review-Prozess begutachten. Die Mathematik steckt also in einer Sackgasse.

"Wir können eine Arbeit von einem Gutachter prüfen lassen - oder: von einem Computer. Macht das einen Unterschied? Ist der Gutachter verlässlicher? Oder der Computer?"

"Zuverlässiger als ein menschlicher Gutachter"

Für Thomas Hales, Mathematiker an der Universität Pittsburgh in Pennsylvania, brachten Computer den Ausweg aus der Sackgasse. Mehrere Jahre hatte er vergeblich darauf gewartet, dass menschliche Gutachter seinen Beweis der Keplerschen Vermutung verifizieren. Am Ende mussten sie kapitulieren. Nicht nur, weil der Beweis aus mehreren hundert Seiten komplexer Geometrie bestand. Zusätzlich waren zehntausende Zeilen Computercode und mehrere Gigabyte Daten Teil des Beweises. Und Mathematiker sind es kaum gewohnt, Computercode auf seine Richtigkeit hin zu überprüfen. Computer kämen mit der Komplexität aber sehr gut klar, sagt Hales.

"Ich behaupte, dass der Computer um viele, viele Größenordnungen zuverlässiger ist als ein menschlicher Gutachter."

Die Systeme, von denen Hales spricht, sind formale Beweisassistenten. Das ist Software, die dabei hilft, einen formalen Beweis aufzubauen. Ein formaler Beweis führt eine Behauptung Schritt für Schritt zurück auf die Grundlagen der Mathematik. Diese Grundlagen, die Axiome, bilden den Kern eines formalen Beweisassistenten. Auf ihnen basiert alles, von ihnen hängt richtig oder falsch ab. Der Kern des Beweisassistenten, den Thomas Hales benutzt, umfasst nur rund 200 Zeilen Programmcode. Diese 200 Zeilen wurden von Mathematikern wieder und wieder auf Fehlerfreiheit überprüft. Sie sind so essenziell, dass manche sie sich sogar auf T-Shirts haben drucken lassen.

Der Beweisassistent hilft dann dabei, all die komplexe Mathematik zu verwalten und zu vernetzen, die Mathematiker aus dem Kern ableiten. So konnte auch Thomas Hales seinen Beweis auf die 200 Zeilen, die Axiome, zurückführen. Am Ende stellte der Computer zweifelsfrei fest, dass der Beweis gültig ist. Ein menschlicher Gutachter ist nur noch nötig, um Bedeutung und Sinnhaftigkeit der Forschungsergebnisse zu beurteilen. Allerdings hat Thomas Hales mit einem Wissenschaftlerteam insgesamt 20 Personenjahre Arbeit investieren müssen. Formale Beweisführung wird aber einfacher werden, sagt Jeremy Avigad, der sich an der Carnegie Mellon University damit beschäftigt.

"Das ist noch eine junge Technik. Sie ist noch schwierig zu benutzen, die Lernkurve ist steil. Man muss die Logik-Sprache lernen und den Umgang mit dem System. Und selbst dann: Ein Theorem zu verifizieren heißt, dass man es sehr viel detaillierter beschreiben muss als bei einem Beweis auf Papier."

Avigad glaubt allerdings, dass es eines Tages Alltag sein wird, dass Computer Beweise verifizieren. Möglicherweise könnten sie sogar selbst neue mathematische Felder erschließen. Und auch in anderen wissenschaftlichen Disziplinen können Beweisassistenten zur Verifikation von Behauptungen genutzt werden. Doch zuerst müssten dazu auch die wissenschaftlichen Publikationsorgane anerkennen, dass Computer unter Umständen die besseren Gutachter sind.

 

Programmtipp
Der Mathemathiker Thomas Hales - Calculemus! Die Kunst, Orangen zu stapeln

(Deutschlandfunk, Wissenschaft im Brennpunkt, 05.04.2015, 16:30 Uhr)

Das könnte sie auch interessieren

Entdecken Sie den Deutschlandfunk