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

Mathematische Unterhaltungen: Hilbert und Isabelle

Eine Gruppe von Jungforschern hat die Lösung für eines der Jahrhundertprobleme des berühmten David Hilbert bestätigt, mit einem Mittel, von dem Hilbert damals nur träumen konnte: einer Software namens Isabelle. Weiteren drei Nachwuchswissenschaftlern gelang es, die für dieses Ergebnis zentralen diophantischen Gleichungen zu optimieren.
Ein Hilbert-Problem mit Software Isabelle gelöstLaden...

Als Thomas Hales 1998 die seit 400 Jahren offene keplersche Vermutung bewies – es ist unmöglich, gleich große Kugeln dichter zu packen, als die Orangenhändler das seit jeher tun –, war zunächst der Jubel groß. Dann kam die Ernüchterung: Der Beweis erstreckte sich nicht nur über mehrere hundert Seiten, sondern war auch so chaotisch formuliert, dass die größten Meister der Mathematik sich außerstande sahen, seine Richtigkeit zu beurteilen.

Die naheliegende Forderung, das ganze Zeug doch einmal ordentlich aufzuschreiben, lehnte Hales zunächst ab. Nochmals mehrere Jahre mit der Bestätigung eines aus seiner Sicht bereits erbrachten Resultats zuzubringen? Da hätte er Besseres zu tun. Aber dann fand er sich doch immerhin bereit, die knechtische Arbeit an einen Computer zu delegieren. Das geht zwar nicht unbedingt schneller: Es ist überaus mühsam, eine Aussage und ihren Beweis so zu formalisieren, dass eine eigens dafür geschriebene Software, ein »Beweisassistent«, jeden einzelnen gedanklichen Schritt auf gewisse Grundaxiome zurückführen und damit verifizieren kann. Aber es verschafft dem ganzen Werk, sei es für Menschen durchschaubar oder auch nicht, den ersehnten Nachweis der Korrektheit. In diesem Fall dauerte es mehr als ein Jahrzehnt: Erst am 14. August 2014 meldete das Projekt Flyspeck (»Fliegenschiss«) Vollzug.

Damit ging, zumindest für diesen Einzelfall, ein Traum des großen Mathematikers David Hilbert in Erfüllung ...

März 2019

Dieser Artikel ist enthalten in Spektrum der Wissenschaft März 2019

Kennen Sie schon …

Spezial Physik - Mathematik - Technik 4/2018

Spektrum der Wissenschaft – Spezial Physik - Mathematik - Technik 4/2018: Faszination Algebra

Komplexe Schönheiten: Funktionen im knallbunten Porträt • Gruppentheorie: Neue Forschungen offenbaren überraschende Verbindungen • Kartenspiel-Algebra: Raffinierte Konstruktionen mit endlichen Körpern

38/2018

Spektrum - Die Woche – 38/2018

In dieser Ausgabe widmen wir uns dem Sommer, dem Altern und Mücken.

Bauch oder Kopf - Wie entscheiden wir?

Spektrum Kompakt – Bauch oder Kopf - Wie entscheiden wir?

Wir nutzen Vernunft und Gefühl, wenn wir Entscheidungen treffen sollen. Doch wie setzen wir Prioritäten, und wie reagieren wir in echten Zwickmühlen? Sind impulsive Menschen weniger rational, und wie gelingt es Marketingexperten, uns subtil zum Kauf zu animieren?

Lesermeinung

Beitrag schreiben

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, Leserzuschriften nicht zu veröffentlichen und Ihre Kommentare redaktionell zu bearbeiten. Die Leserzuschriften 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 Teilnehmer sich leichter auf Ihre Beiträge beziehen können. Ausgewählte Lesermeinungen können ohne separate Rücksprache auch in unseren gedruckten und digitalen Magazinen veröffentlicht werden. Vielen Dank!

  • Quellen

Jones, J. P. et al.: Diophantine Representation of the Set of Prime Numbers. In: The American Mathematical Monthly 83, S. 449–464, 1976

Matiyasevich, Y.: On Hilbert's Tenth Problem. Pacific Institute for the Mathematical Scences, 2000

Andrew Gilroy: Undecidability in Number Theory. 2008

Jugend forscht Bundessieger starten beim EU-Wettbewerb 2018 und messen sich mit Europas besten Nachwuchswissenschaftlern. Pressemitteilung vom 13. 9. 18