Direkt zum Inhalt
Login erforderlich
Dieser Artikel ist Abonnenten mit Zugriffsrechten für diese Ausgabe frei zugänglich.

Informatik: Mathematiker aus Silizium

Ein Computer, der eigenständig mathema­tische Vermutungen formuliert und diese auch beweist – davon träumen viele Wissenschaftler. Neue Methoden der künstlichen Intelligenz könnten die Zukunftsvision ein Stück näher bringen.
Roboter in Denkerpose

»Zu einem unbestimmten zukünftigen Zeitpunkt werden Mathematiker durch Computer ersetzt.« Die gewagte Vorhersage soll der renommierte Mathematiker Paul Cohen (1934–2007) Berichten zufolge in den 1970er Jahren gemacht haben. Bis heute stößt die Äußerung bei seinen Kollegen auf Gegenwind. Cohen war schon immer ein Querdenker: Seine revolutionären Methoden in der Mengenlehre brachten ihm die Fields-Medaille ein, damit ist er die erste und bisher einzige Person, welche die begehrte Auszeichnung für Arbeiten in der Logik erhalten hat. Zudem vertrat er die kontroverse Meinung, die gesamte Mathematik ließe sich automatisieren, einschließlich des Führens von Beweisen.

Anders als man durch die Erfahrungen aus dem Mathematikunterricht vielleicht denken mag, besteht die Arbeit eines Mathematikers nicht darin, zu rechnen. Seine Hauptaufgabe ist es, formale Aussagen unwiderruflich zu belegen. Ein Beweis ist ein schrittweise geführtes logisches Argument, das überprüft, ob eine Vermutung wahr ist. So- bald sie bewiesen ist, wird eine Vermutung zu einem Theorem (auch Satz genannt). Darüber hinaus erklären Beweise, warum eine Aussage gültig – oder falsch – ist. Gleichwohl sind sie schwer zu fassen, denn die Argumente bewegen sich in einer extrem abstrakten Welt, die nichts mit unseren alltäglichen Erfahrungen zu tun haben. »Wir Menschen sind für die Art von Aufgabe nicht geeignet«, sagt der Kognitionswissenschaftler Simon DeDeo von der Carnegie Mellon University in Pittsburgh.

Bisher setzt man Computer meist ein, um große Berechnungen durchzuführen. Aber Mathematik erfordert etwas anderes. Vermutungen entstehen durch induktives Denken, eine Person muss sich intuitiv über ein interessantes Problem Gedanken machen. Beweise folgen meist einer deduktiven, schrittweisen Logik. Dazu verbindet man häufig komplizierte Zusammenhänge auf kreative Weise und füllt mühsam anschließend alle vorhandenen Argumenta­tionslücken. Maschinen können solche Aufgaben bisher noch nicht meistern.

Dennoch gibt erste Ansätze, wie Algorithmen die Arbeit von Mathematikern unterstützen können …

Kennen Sie schon …

Spektrum - Die Woche – Kerzenchemie

Heiligabend gemütlich bei Kerzenschein zusammensitzen? Ja, aber besser nicht zu viele Kerzen – und danach einmal kräftig durchlüften, wie unsere Weihnachtstitelgeschichte erläutert. Außerdem: In der Nordsee schwimmen wieder Seepferdchen. Und Astronaut Matthias Maurer erzählt über Raumanzüge.

Spektrum der Wissenschaft – Mathematik für die Zukunft

In »Mathematik für die Zukunft« stellen wir den neuen Formalismus der verdichteten Mengen vor, der von Peter Scholze und Dustin Clausen entworfen wurde. Daneben: Evolution der Säugetiere, rätselhafte Radioblitze, Funde in Jerusalem.

Spektrum - Die Woche – Drohen im Winter Stromausfälle?

Deutschlands Stromnetz scheint am Limit – doch die Netzbetreiber halten die Gefahr von Stromausfällen derzeit für gering. Die Herausforderungen werden nach dem Winter jedoch nur noch größer. Außerdem in dieser Ausgabe: Sind blaue Räume besser als grüne? Und wie erschafft man unknackbare Funktionen?

Schreiben Sie uns!

1 Beitrag anzeigen

Wir freuen uns über Ihre Beiträge zu unseren Artikeln und wünschen Ihnen viel Spaß beim Gedankenaustausch auf unseren Seiten! Bitte beachten Sie dabei unsere Kommentarrichtlinien.

Tragen Sie bitte nur Relevantes zum Thema des jeweiligen Artikels vor, und wahren Sie einen respektvollen Umgangston. Die Redaktion behält sich vor, Zuschriften nicht zu veröffentlichen und Ihre Kommentare redaktionell zu bearbeiten. Die Zuschriften können daher leider nicht immer sofort veröffentlicht werden. Bitte geben Sie einen Namen an und Ihren Zuschriften stets eine aussagekräftige Überschrift, damit bei Onlinediskussionen andere Teilnehmende sich leichter auf Ihre Beiträge beziehen können. Ausgewählte Zuschriften können ohne separate Rücksprache auch in unseren gedruckten und digitalen Magazinen veröffentlicht werden. Vielen Dank!

  • Quellen

Chlipala, A.: Proof assistants at the hardware-software interface. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

Hales, T. C.: A proof of the Kepler conjecture. Annals of mathematics 162, 2005

Rabe, M. N. et al.: Mathematical reasoning via self-supervised skip-tree training. ArXiv 2006.04757, 2020

Urban, J., Jakubův, J.: First neural conjecturing datasets and experiments. In: Benzmüller C., Miller, B. (Hg.) Intelligent computer mathematics. Springer Cham, 2020

Viteri, S., DeDeo, S.: Explosive proofs of mathematical truths. ArXiv 2004.00055, 2020