In einem geheimnisvollen Bereich der Informatik wurde kürzlich ein vierzig Jahre altes Rätsel – das Busy-Beaver-Problem – von einer Gruppe von Hobbyisten gelöst. Diese Leistung hat nicht nur in der akademischen Welt für Aufsehen gesorgt, sondern wurde auch von dem berühmten Mathematiker Terence Tao gewürdigt, der die Nachricht in den sozialen Medien teilte und die Bedeutung von Beweisassistenten in der mathematischen Forschung hervorhob.
Der Informatiker Scott Aaronson lobte diese Entdeckung ebenfalls hoch und bezeichnete sie als den wichtigsten Fortschritt in der Erforschung der Busy-Beaver-Funktion seit 1983. Dieser Erfolg markiert ein tieferes Verständnis der Grenzen der Berechnungstheorie und zeigt das Potenzial softwaregestützter Beweise bei der Lösung komplexer mathematischer Probleme.
Das Busy-Beaver-Problem entstand vor über 40 Jahren in Dortmund, Deutschland, als Informatiker versuchten, eine bestimmte Turingmaschine zu finden, die vor dem Anhalten die meisten „1en“ schreiben kann. Eine Turingmaschine ist ein abstraktes Berechnungsmodell, das 1936 von Alan Turing vorgestellt wurde und Berechnungen durch Lesen und Schreiben von 0en und 1en auf einem unendlich langen Band durchführt.
Nachdem 1974 die vierte Busy-Beaver-Zahl bestimmt wurde, blieb die Suche nach der fünften eine offene Frage. Jetzt hat eine Online-Community aus über 20 Beiträgern aus aller Welt unter Verwendung der Beweisassistenten-Software Coq den Wert der fünften Busy-Beaver-Zahl BB(5) mit 47.176.870 erfolgreich verifiziert.
Diese Leistung hat nicht nur die Community begeistert, sondern auch den Informatiker Damien Woods in Erstaunen versetzt, der diesen Fortschritt mit der Geschwindigkeit von Usain Bolt verglich. Obwohl die Lösung dieses Problems möglicherweise nicht direkt auf andere Bereiche der Informatik angewendet werden kann, ist der Kampf gegen die mathematische Unmöglichkeit selbst die größte Belohnung für die Teilnehmer.
Der Kern des Busy-Beaver-Problems liegt im Verständnis des Verhaltens von Turingmaschinen, insbesondere ihres Verhaltens beim Halteproblem. Das Verhalten einer Turingmaschine wird durch eine Reihe von Regeln definiert, die man sich als Tabelle vorstellen kann. Jede Regel gibt an, welche Aktion der Lese-/Schreibkopf bei einer 0 oder 1 in einem bestimmten Zustand ausführen soll.
Obwohl Turingmaschinen in eine Endlosschleife geraten können, ist die Bestimmung, ob sie anhalten oder nicht, ein bekanntes ungelöstes Problem. Der Mathematiker Tibor Radó war mit dieser Schlussfolgerung nicht zufrieden und erfand das „Busy-Beaver-Spiel“, um das Wesen des Halteproblems zu untersuchen, indem er Turingmaschinen nach der Anzahl ihrer Regeln gruppierte.
Frühe Forscher wie Allen Brady untersuchten dieses Problem, indem sie Programme schrieben, die das Verhalten von Turingmaschinen simulierten. Seine Arbeit und die Erkenntnisse anderer Forscher bildeten die Grundlage für spätere Forschungen.
Bis 2022 initiierte der Doktorand Tristan Stérin die „Busy-Beaver-Challenge“, ein Online-Kooperationsprojekt, das darauf abzielte, BB(5) endgültig zu bestimmen. Mit innovativen Methoden und der Hilfe des Coq-Beweisassistenten fand das Team schließlich die fünfte Busy-Beaver-Zahl.
Diese Leistung ist nicht nur eine Herausforderung für die mathematische Unmöglichkeit, sondern auch eine Erkundung der Grenzen der Informatik. Mit der Bestätigung von BB(5) verfassen die Forscher derzeit einen wissenschaftlichen Artikel, der eine menschenlesbare Version des Coq-Beweises sein wird. Gleichzeitig überlegen sie, ob die Erforschung von BB(6) das nächste Ziel sein wird.
Referenzen: https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/