Beweis-Software Sind Computer die besseren Mathematiker?

Große Ideen entstehen im Kopf - so meinen viele Mathematiker. Doch das könnte sich ändern, wenn Software eines Tages beginnt, eigenständig Probleme zu lösen.

Denkende Maschine: "Das ist eine Revolution"
Corbis

Denkende Maschine: "Das ist eine Revolution"

Von


Wir Menschen sind lausige Rechner. Bei Aufgaben wie 141 durch 3 müssen wir kurz überlegen. 120 durch 3 - das ist 40. Und 21 durch 3 ist 7 - macht zusammen 47. Jeder Computer, jeder 20 Jahre alte Taschenrechner ist schneller. Aber sobald es um mehr geht als stumpfes Addieren oder Dividieren, stoßen Computer an ihre Grenzen.

Welches Programm etwa könnte auf Knopfdruck prüfen, ob der Lösungsweg eines Schülers bei der schriftlichen Abiprüfung stimmt? Und welche Software kann Vermutungen beweisen, an denen bereits Generationen von Mathematikern verzweifelt sind? Ohne den menschlichen Geist, so scheint es, geht kaum etwas.

Doch es gibt Informatiker und Mathematiker, die Gehirnen nur noch eine Nebenrolle in der Zukunft der Mathematik zuschreiben. Timothy Gowers von der University of Cambridge etwa, Begründer der Plattform Polymath, sagt: "In 25 Jahren werden Computer nützliche Assistenten von Mathematikern sein. In 50 Jahren werden Computer besser Mathematik betreiben als Menschen." Hat der Träger der renommierten Fields-Medaille recht?

Über diese Frage diskutierten mehr als hundert Wissenschaftler auf dem Kongress CADE-25 in Berlin, der am Freitag zu Ende ging. Die meisten sind Informatiker. Und sie wissen, dass sich die Art, Mathematik zu betreiben, in den kommenden Jahren verändern wird. Genies, die allein mit Stift und Papier große Rätsel lösen, wird es künftig womöglich nur noch selten geben.

Formale Logik gut geeignet

"Wir nähern uns der Situation, in der Software wissenschaftliche Aufsätze prüft", sagt Christoph Benzmüller von der FU Berlin. Er hat kürzlich gemeinsam mit Kollegen einen Gottesbeweis von Kurt Gödel am Computer nachvollzogen. Aus wenigen Grundannahmen und mithilfe strenger Logik leitete die Software her, dass Gott "notwendigerweise" existiert. "Solche auf formaler Logik basierende Beweise eignen sich besonders gut für eine Umsetzung am Computer", erklärt Benzmüller.

Beweise zu finden, sei inzwischen per Software möglich, solange im Beweis nicht mehrere mathematische Teilgebiete wie Algebra und Gruppentheorie kombiniert werden müssten. "Das ist eine Revolution", ergänzt Reiner Hähnle von der TU Darmstadt. "Beweise bestanden über Jahrhunderte darin, andere Menschen mit präzisen Argumenten zu überzeugen." Nun komme Software ins Spiel, die viel weniger anfällig für Fehler sei als der Mensch.

Beim Beweisen per Software gibt es zwei Spielarten. Entweder ein Programm überprüft eine existierende, in der Regel von Menschen gefundene Lösung (Proof Checker). Oder aber, und das ist deutlich anspruchsvoller, Software sucht eigenständig nach einem Beweis (Theorem Prover). Sie muss dabei verschiedene Wege ausprobieren und kann auch Ideen früherer Beweise nutzen, mit denen sie vorab gefüttert wurde.

Kugeln dicht packen

Der Mathematiker Thomas Hales hat bereits gezeigt, dass Software sehr schwierige Probleme knacken kann. 1999 bewies er die Kepler-Vermutung mit komplizierten Computerberechnungen. Dabei geht es um die Frage, wie dicht man Kugeln im Raum packen kann. Hales reduzierte das Problem auf 2500 verschiedene Kugelanordnungen, die er dann von einem Computer einzeln überprüfen ließ. Die Arbeit fand jedoch keine rechte Anerkennung unter Kollegen, weil sie kaum nachvollziehen konnten, was die Software genau gemacht hatte.

Das wurmte Hales so sehr, dass er 2014 seinen Computerbeweis von 1999 mit einem Proof Checker überprüfte. Damit konnte er zeigen, dass jeder einzelne Beweisschritt logisch konsistent war - und damit auch der gesamte Beweis.

Trotz solcher Erfolge bleibt mancher Mathematiker skeptisch gegenüber Computerbeweisen, denn sie passen nicht so recht zum eigenen Selbstverständnis. Hélène Esnault von der FU Berlin etwa hält wenig vom Hype: "Mathematik ist ein intellektueller Prozess und findet zuallererst im Kopf statt." Die kreativen, neuartigen Ideen, die man braucht, um schwierige mathematische Probleme zu lösen, traut sie Computerprogrammen bislang kaum zu.

Christoph Benzmüller widerspricht: "Dass Computer nicht intuitiv sind, hat noch niemand bewiesen." Seine Euphorie wurde allerdings nicht von allen Kongressteilnehmern in Berlin geteilt. "Wir werden so schnell nicht erleben, dass Computer die besseren Mathematiker sind", meint Reiner Hähnle von der TU Darmstadt. Programme würden zu intelligenten Assistenten, die Mathematikern viele Routineaufgaben abnehmen könnten. "Echte Kreativität zu entwickeln, ist aber nach wie vor eine große Herausforderung."

Kurzfristig werden wohl Proof Checker Mathematikern die größte Hilfe bieten. Solche Beweisprüfer könnten nämlich eines ihrer drängendsten Probleme lösen: die immer umfangreicheren und immer komplizierteren Beweise checken.

Der Japaner Shinichi Mochizuki etwa hatte 2012 einen mehrere Hundert Seiten umfassenden Beweis für ein uraltes Zahlenrätsel vorgelegt - die abc-Vermutung. Doch anerkannt ist seine Arbeit bis heute nicht. Die rund 500 Seiten kritisch durchzuarbeiten, ist ein zeitraubendes Unterfangen. Könnten Computer diese Prüfung übernehmen, wäre allen geholfen.

Mehr zum Thema


Forum - Diskutieren Sie über diesen Artikel
insgesamt 109 Beiträge
Alle Kommentare öffnen
Seite 1
der_neue_Student 08.08.2015
1. das Elektronengehirn
gibt es nicht! Leider lässt sich dieser Mythos nicht nicht ausrotten :-) Wie gesagt, das Problem der dichtesten Packung hatte schon Keppler vor fast 300 Jahren gelöst.
braindead0815 08.08.2015
2. Echte Kreativität zu entwickeln, ist aber nach wie vor eine große Herausforderung.
das wäre die "KI" nur im film zu realisieren, genau wie die lichtgeschwindigkeit (warp scooty beam me up) der mensch sollte sich (falls es überhaupt zu realisieren wäre) überlegen, was er damit anfangen will, wozu warum und wie sich das gesellschaftlich lösen soll, wenn es schon probleme mit ausländern - flüchtlingen usw gibt.
Ureinwohner2.0 08.08.2015
3. Der Computer macht das...
Die Rechenmaschinen tun genau das, was kluge Menschen ihm "eingehaucht" haben (via "Computerprogramm") - nicht weniger, aber auch nicht mehr. Es wird also immer kluger Programmierer bedürfen, um die Maschinen "intellegent" erscheinen zu lassen. Sollte es tatsächlich irgendwann in fernen Zukunft selbstoptimierende Computerprogramme geben, dann sollten die klügsten Menschen schnell die Stecker aus der Steckdose ziehen. Evolution 4.0 könnte sonst die Menschheit ausrotten, denn Menschen wären nicht optimal genug, um bestehen zu können. :-(
MatthiasPetersbach 08.08.2015
4.
wenn die software mal fähig wäre, die EIGENEN probleme zu lösen, wäre schon viel gewonnen
gingermath 08.08.2015
5.
Nur weil sie jetzt in der Lage sind, nicht nur 1 + 1 zusammen zu zählen, sondern auch Folgerungen aus a folgt b zu lösen, werden sie Mathematiker nicht ersetzen können. Irgendjemand musste ihnen ja erklären, was a bzw. b ist, und dass aus a gleich b folgt. Vielleicht werden sie ja mal irgendwann mehr sein, als eine reine Ansammlung von Informationen, die in unterschiedlicher Weise abgespielt werden, bis dahin ist aber noch viel zeit.
Alle Kommentare öffnen
Seite 1

© SPIEGEL ONLINE 2015
Alle Rechte vorbehalten
Vervielfältigung nur mit Genehmigung der SPIEGELnet GmbH


TOP
Die Homepage wurde aktualisiert. Jetzt aufrufen.
Hinweis nicht mehr anzeigen.