Der Traum von der Beweismaschine 

Warum die Arbeit der Mathematiker nicht überflüssig wird

KI-Systeme, die neuerdings gleich industriell Beweise für ungelöste mathematische Probleme liefern, wecken ein ambivalentes Gefühl: den Traum einer Beweismaschine und die Befürchtung, dass durch sie die Arbeit der Mathematiker überflüssig würde. Beides beruht auf frag-würdigen Annahmen. 

Die erste lautet, etwas salopp formuliert: Mathematik ist eine monumentale Sammlung bewiesener oder beweisbarer Sätze. Hinter dieser Annahme steckt eine ganze Metaphysik. Ersonnen hat sie das Universalgenie Gottfried Wilhelm Leibniz mit seiner grandiosen Idee, dass die Welt berechenbar sei – geschaffen von einem, wie man heute sagen würde, obersten Softwareingenieur. Leibniz hatte eine zweite grandiose Idee, nämlich, dass sich eine Kunstsprache – ein Calculus ratiocinator – konstruieren lasse, in der man den Wahrheitsgehalt eines Satzes durch reine mechanische Prozedur ermitteln kann. Ein Gedanke, der seither seine Spur unauslöschlich in die Mathematikerköpfe eingraviert hat.

***

Zu Beginn des 20. Jahrhunderts suchten die Mathematiker, ihre Disziplin durch ein robustes logisches Fundament zu begründen. Das Leibnizsche Ideal eines Calculus ratiocinator nahm dabei die neue Gestalt eines formalen Systems an, in das sich alle mathematischen Sätze übersetzen lassen.  Ihre Geltung würde dann in der deduktiven Herleitung aus Axiomen bestehen.  Einer der Wortführer dieses Projekts, David Hilbert, war überzeugt, dass zumindest in der Mathematik alle wahren Sätze durch eine solche logische Maschine beweisbar sind. Diese Zuversicht in die menschliche Erkenntniskraft ist auf seinem Grabstein eingemeisselt: «Wir müssen wissen. Wir werden wissen». 

Dieser Zuversicht versetzte ein junger österreichischer Mathematiker einen schweren Schlag: Kurt Gödel. Anfang der 1930er Jahre zeigte er, dass jedes hinreichend leistungsfähige, widerspruchsfreie und formal axiomatisierte System Aussagen enthält, die sich innerhalb des Systems weder beweisen noch widerlegen lassen. Gödel lieferte damit gewissermassen eine Kritik der formalen Vernunft. Sie widerlegt nicht die Möglichkeit mathematischer Beweismaschinen. Sie erschüttert vielmehr den Traum, die mathematische Wahrheit lasse sich in einem einzigen formalen System vollständig einfangen.

***

Der Traum von der Beweismaschine lebt weiter. Er ist von der Theorie in die Technologie gewandert. In den grossen Sprachmodellen – den Large Language Models (LLMs) – scheint er eine neue Gestalt anzunehmen. Sprachmodelle können mathematische Probleme lösen, Beweise entwickeln und ihre eigenen Lösungswege überprüfen lassen. Aber sie werfen eine alte, nun umso dringlichere Frage auf: Was ist ein Beweis? 

Die Frage erinnert an den Supercomputer Deep Thought in Douglas Adams’ Kultroman «Per Anhalter durch die Galaxis». Auf die Frage nach dem Sinn des Lebens, des Universums und des ganzen Rests gibt der Computer nach einer Rechenzeit von 7.5 Millionen Jahren die Ant-wort «42» heraus. Der Haken: Niemand versteht sie. 

Hier kommt ein weiterer Irrtum zum Vorschein: Es genügt nicht, dass ein Beweis logisch korrekt ist. Er sollte auch verständlich machen, weshalb eine Aussage gilt. Wenn dies schon unter Mathematikern nicht immer gelingt, verschärfen KI-Systeme das Problem noch: Sie spucken zunehmend Beweise aus, deren Nachvollzug den Mathematikern ironischerweise zusätzliche Interpretationsanstrengung abverlangt. 

***

Das heisst, wir haben es nicht bloss mit einem technischen, sondern mit einem erkenntnis-theoretischen Problem zu tun: Wollen wir bloss richtige Antworten erhalten, oder wollen wir verstehen, weshalb sie richtig sind? Eine Maschine, die uns die Lösung liefert, dispensiert uns möglicherweise gerade von jener geistigen Arbeit, die Information zu Einsicht raffiniert. Der Fields-Medaillenträger Hugo Duminil-Copin von der Universität Genf hat dies auf den Punkt gebracht: Sich mit einem Helikopter auf dem Mount Everest abzusetzen, ist etwas anderes als ihn zu besteigen. 

Mathematik ist eine soziale Tätigkeit. Mathematiker wollen ihre Kollegen interessieren, irritieren, ja infizieren. Je schwieriger ein Problem, desto grösser die Reputation, die seine Lösung verspricht, desto ausgeprägter die Distinktion. Nun sehen sich Lösungen der mathematischen «Haute Couture» durch Lösungen «von der Stange» bedroht. Akshay Venkatesh vom Institute for Advanced Study in Princeton – auch er Fields-Medaillenträger – befürchtet so-gar, dass die Mathematik für die nächste Generation an Attraktivität verlieren könnte. Man mag darin auch den üblichen «zünftlerischen» Konservatismus oder einen gewissen Elitismus erkennen. Entscheidend aber ist eine andere Frage: Wie lässt sich gewährleisten, dass Ma-thematik eine intellektuelle Allmende bleibt – ein gemeinsames Gut, an dem möglichst viele nicht nur teilhaben, sondern zu dessen Weiterentwicklung sie auch beitragen können?

***

Ein anderer Irrtum: Beweise schliessen einen Denkvorgang ab – quod erat demonstrandum, wie die lateinische Formel unmissverständlich verkündet. Das Gegenteil ist oft der Fall: ein Beweis schliesst auf. 

Betrachten wir Euklids Beweis, dass es unendlich viele Primzahlen gibt. Nehmen wir an, alle Primzahlen liessen sich in einer endlichen Liste aufzählen. Wir multiplizieren die Zahlen dieser Liste miteinander und addieren eins. Bei den ersten vier Primzahlen, 2, 3, 5 und 7, erhalten wir 211 – selbst eine Primzahl, die in der Liste fehlt. Allgemein muss die so gebildete Zahl nicht prim sein. Nehmen wir etwa die Primzahlen 2, 3, 5, 7, 11 und 13: Ihr Produkt plus eins ist 30031, das sich in 59 und 509 zerlegen lässt. Beide Primteiler fehlen in der Ausgangsliste. Das widerspricht der Annahme, die Liste enthalte alle Primzahlen.

Das Verfahren liefert nicht nur einen Beweis, es ist die Blaupause für Konstruktionen, mit denen sich auch auf anderen Gebieten Unbegrenztheiten erschliessen lassen. Sie machen überhaupt erst denkbar, was vorher undenkbar war. 

***

Hier liegt ein weiterer Irrtum: Mathematik löst nicht nur Probleme – sie bringt auch neue hervor. Sie ist eine Kunst des Vermutens – «Ars Conjectandi» -, wie sie der grosse Basler Gelehrte Jakob Bernoulli nannte. Und so gesehen, steht sie als Gegenbegriff zur Antwortproduktion der KI-Systeme. Denn mathematisches Denken besteht nicht allein darin, Lösungen zu finden. Es besteht ebenso darin, Fragen zu entdecken, Vermutungen zu wagen und Probleme zu formulieren, von denen man zuvor nicht einmal wusste, dass sie sich stellen.

Deshalb wage ich eine kühn erscheinende These: Mathematik ist poetisch. Das altgriechische poiein bedeutet «machen, hervorbringen, erschaffen». Mathematik bringt Denkräume her-vor. Sie beschäftigt sich mit Unendlichkeiten, und seit Georg Cantor sogar mit unendlich vielen. Sie konzipiert Geometrien, in denen sich zwei parallele Geraden schneiden. Sie rechnet mit Zahlen, die «imaginär» sind. Sie zaubert aus einer einfachen Formel eine ganze Welt komplexer fraktaler Strukturen. 

Das Vermögen der Sprache erlaubt dem Menschen ein diskursives Verständnis der Welt - aber mehr noch: Er kann mit Sprachen Welten schaffen, die sein Verständnis womöglich übersteigen. Gottfried Benn hat dies in einem wunderschönen Aphorismus verdichtet: «(Es) gibt nur zwei verbale Transzendenzen: die mathematischen Lehrsätze und das Wort als Kunst. Alles andere ist Geschäftssprache, Bierbestellung». Das heisst: Poesie führt über den gewohnten Sprachgebrauch hinaus – und Mathematik führt über den gewohnten Denkgebrauch hinaus. 

***

Die Mathematik kennt zahlreiche Vermutungen, für die bislang kein Beweis gefunden wurde. Manche könnten sich als wahr erweisen, andere als falsch; bei manchen bleibt die Antwort womöglich offen. So wie in der Thermodynamik ein Perpetuum mobile unmöglich ist, gibt es auch kein «Perpetuum demonstrans» in der Mathematik: keinen universellen Beweisautomaten, der in einem hinreichend leistungsfähigen formalen System jede wahre mathematische Aussage beweisen könnte. Die Mathematik bleibt ein unerschlossenes geistiges Land. Ein Jahrhundert nach Hilbert kann man ihm erwidern: Wir werden nicht wissen.