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?"

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.