1 Punkte von GN⁺ 2024-07-03 | 1 Kommentare | Auf WhatsApp teilen
  • Einführung

    • Vor 40 Jahren trafen sich in Dortmund Informatiker, um den fünften Busy Beaver zu finden.
    • Busy Beaver sind einfache Computerprogramme, deren Laufzeit sehr lang werden kann.
    • Diese Programme stehen in Zusammenhang mit berühmten ungelösten Problemen der Mathematik und gehen auf ein altes Problem der Informatik zurück.
    • Vor zwei Jahren startete der Doktorand Tristan Stérin die Busy-Beaver-Challenge, an der sich weltweit mehr als 20 Mitwirkende beteiligten.
    • Heute hat das Team den Wert von BB(5) mit 47.176.870 bestätigt.
  • Anhalten oder nicht anhalten

    • Busy-Beaver-Programme werden als Anweisungen für einen theoretischen Computer geschrieben, die sogenannte Turing-Maschine.
    • Eine Turing-Maschine führt Berechnungen aus, indem sie auf einem unendlichen Band 0 und 1 liest und schreibt.
    • Das Problem vorherzusagen, ob eine Turing-Maschine anhält oder für immer weiterläuft, nennt man das Halteproblem.
    • Für das Halteproblem gibt es keine allgemeine Lösung, was die Jagd nach Busy Beavern noch attraktiver macht.
  • Das Auftauchen des Beavers

    • Der Mathematiker Tibor Radó erfand 1962 das Busy-Beaver-Spiel.
    • Die Turing-Maschine, die innerhalb einer jeweiligen Regelgruppe am längsten läuft, wird Busy Beaver genannt.
    • BB(n) bezeichnet die Anzahl der Schritte, die eine Busy-Beaver-Maschine mit n Regeln ausführt, bevor sie anhält.
  • Bradys Beaver-Herde

    • Allen Brady entwickelte in den 1960er Jahren Techniken zur Busy-Beaver-Suche und bestimmte 1974 den Wert des vierten Busy Beavers.
    • BB(4) wurde als Maschine bestätigt, die nach 107 Schritten anhält.
  • Der fünfte Beaver

    • Beim Wettbewerb 1984 in Dortmund begann die erste große Suche nach dem fünften Busy Beaver.
    • 1989 entdeckte Heiner Marxen eine Maschine, die nach 47.176.870 Schritten anhält.
    • 2003 brach Georgi Georgiev die Suche nach BB(5) ab und hinterließ 43 ungelöste Turing-Maschinen.
  • Aufruf an alle Jäger

    • Tristan Stérin startete 2022 die Busy-Beaver-Challenge, an der sich Mitwirkende aus aller Welt beteiligten.
    • Shawn Ligocki stieß 2022 zum Team und leistete wichtige Beiträge.
    • Justin Blanchard entwickelte mit der Methode der Closed Tape Language einen der stärksten Ansätze des Teams.
  • Annäherung an das Monster

    • Skelet #1 und #17 waren besonders schwierige Maschinen, und das Team kombinierte verschiedene Ideen, um sie zu lösen.
    • Im Mai 2023 vollendete ein anonymer Mitwirkender namens mxdys den Coq-Beweis.
  • Wo die Beaver umherstreifen

    • Das Team arbeitet derzeit an einer formalen wissenschaftlichen Veröffentlichung, und einige bemühen sich bereits darum, den nächsten Beaver zu finden.
    • BB(6) dürfte sich wegen eines Problems ähnlich der Collatz-Vermutung als schwer lösbar erweisen.

Meinung von GN⁺

  • Dieser Artikel bietet ein faszinierendes Beispiel für die Erforschung der Grenzen der Informatik.
  • Die Busy-Beaver-Challenge zeigt, wie wichtig kollaborative Forschung ist.
  • Die Lösung von BB(5) hat große Bedeutung für die Informatik- und Mathematik-Community.
  • Ein ähnliches Projekt ist die Forschung zur Collatz-Vermutung.
  • Bei der Einführung neuer Technologien oder von Open Source sind Zusammenarbeit und Reproduzierbarkeit wichtig.

1 Kommentare

 
GN⁺ 2024-07-03
Hacker-News-Kommentare
  • Es wurden Kommentare zu einem Blogbeitrag von Scott Aaronson geteilt.

    • Ein Link zu einem früheren verwandten Thread wurde bereitgestellt.
  • Es gibt verschiedene Varianten des Busy-Beaver-Problems.

    • Es gibt eine Variante, die Lambda-Kalkül verwendet.
    • Es gibt eine Variante, die über Kolmogorov-Komplexität ausgedrückt wird.
  • Es wurde die Geschichte eines Ingenieurs geteilt, der seinen Job kündigte, um das Busy-Beaver-Problem zu erforschen.

    • Es wird gefragt, ob dieser Ingenieur mxdys ist.
  • Es gibt eine Erwähnung eines Coq-Beweises.

    • Es wird die Möglichkeit aufgeworfen, dass es sich nicht um einen von Grund auf geordneten Beweis handelt, sondern um den ersten geordneten Beweis.
  • Es gibt die Meinung, dass Tibor Radós ursprüngliche Busy-Beaver-Arbeit leicht zu lesen und unterhaltsam ist.

    • Ein Link zu einer modernen Version der Arbeit wurde bereitgestellt.
  • Das Halteproblem für Turing-Maschinen-Programme mit 5 Zuständen und 2 Farben wurde gelöst.

    • Es wird die Frage aufgeworfen, ob dies auch auf den Fall mit 2 Zuständen und 4 Farben anwendbar ist.
  • Es wird auf die falsche Vorstellung hingewiesen, dass Menschen das Halteproblem intuitiv lösen könnten.

  • Es wurde die Erfahrung geteilt, in einem privaten Projekt ein Programm zur Lösung des Cutting-Stock-Problems geschrieben zu haben.

    • Dabei wurden ähnliche Optimierungsmethoden wie in Bradys Programm verwendet.
  • Es gibt die Meinung, dass es Glück war, beweisen zu können, ob Programme von Turing-Maschinen mit 5 Zuständen halten.

  • Laut Scott Aaronsons Blogbeitrag gibt es 16.679.880.978.201 Turing-Maschinen mit 5 Zuständen.

    • Es wird gefragt, wie viel Prozent davon anhalten.
  • Die Werte der Busy-Beaver-Funktion wurden geteilt.

    • BB(5) wurde als 47.176.870 bewiesen.
    • BB(6) ist mindestens 10^10^...^10 (ein Exponentialturm mit 15 Stufen).