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öst

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 ...

Kennen Sie schon …

Spektrum Kompakt – Kryptografie - Sicher kommunizieren

Sichere Passwörter, sichere Messenger, sichere Datenübertragung - in Zeiten digitaler Kommunikation spielt der Schutz der übermittelten Inhalte eine große Rolle. Wie gelingt er?

Spektrum Kompakt – Quantencomputer - Der Weg in die praktische Anwendung

Im Jahr 2019 präsentierte Google den ersten Quantencomputer, der klassische Rechner übertrumpfen sollte. Mit weiteren Unternehmen wie IBM liefert sich der Konzern ein Rennen um die Frage: Wie schnell wird die Technologie die Praxis erobern?

Spektrum der Wissenschaft – 2/2021

In dieser Ausgabe widmet sich Spektrum der Wissenschaft dem Thema Größe unendlicher Mengen. Außerdem im Heft: Marserkundung mit drei Raumsonden, fünf Klimamodelle, Soziale Landkarten im Gehirn.

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