Forschende nähern sich mit dem fünften Busy Beaver der Grenze des Berechenbaren
(quantamagazine.org)- Die Busy Beaver Challenge, an der sich weltweit mehr als 20 Personen beteiligten, hat die Busy-Beaver-Zahl für Turing-Maschinen mit 5 Regeln BB(5)=47.176.870 verifiziert
- Damit ist bestätigt, dass die 1989 von Marxen und Buntrock gefundene Maschine, die nach 47.176.870 Schritten anhält, tatsächlich die am längsten laufende 5-Regel-Haltemaschine ist
- Das Team kombinierte einen Genealogie-Ansatz zur Reduktion redundanter Kandidaten, Programme zum Nachweis von Nicht-Halten und den Coq-Proof-Assistant, um zig Millionen Kandidaten zu verarbeiten
- Das Endergebnis wurde als 40.000 Zeilen umfassender Coq-Beweis von mxdys fertiggestellt, der Techniken aus der Community zusammenführte, und vom Coq-Experten Yannick Forster von Inria geprüft
- Bei BB(6) taucht mit der 6-Regel-Maschine Antihydra, die der Collatz conjecture ähnelt, eine Barriere auf, weshalb BB(5) möglicherweise die letzte Busy-Beaver-Zahl ist, die die Menschheit exakt kennen wird
BB(5) ist bestätigt
- Das Team der Busy Beaver Challenge hat den exakten Wert von BB(5) als 47.176.870 verifiziert
- Dieser Wert bezeichnet die maximale Anzahl an Schritten, die eine haltende Turing-Maschine mit 5 Regeln ausführen kann
- Für die Verifikation wurde der Coq proof assistant verwendet; Coq zertifiziert, dass ein mathematischer Beweis fehlerfrei aufgebaut wurde
- Cristopher Moore vom Santa Fe Institute bezeichnete die soziale und mathematische Ingenieursleistung hinter der Arbeit als beeindruckend
- Damien Woods von der Maynooth University verglich die Geschwindigkeit des Ergebnisses mit „Usain-Bolt-Territorium“
- Der entscheidende Punkt an BB(5) ist weniger eine Anwendung in anderen Teilgebieten der Informatik als vielmehr der Erfolg an der Grenze der Unberechenbarkeit
Das Busy-Beaver-Problem und das Halteproblem
- Das Busy-Beaver-Problem betrachtet keine allgemeinen Programmiersprachen, sondern Turing-Maschinen
- Turing-Maschinen lesen und schreiben 0 und 1 auf einem unendlichen Band; dabei bewegt sich der Kopf Feld für Feld und arbeitet nach einer Regeltabelle
- Jede Regel legt abhängig davon, ob aktuell 0 oder 1 gelesen wird, die nächste Aktion fest
- Sie verändert den Wert oder lässt ihn unverändert
- Sie bewegt sich nach links oder rechts
- Sie bestimmt die nächste Regel, auf die verwiesen wird
- Eine spezielle Regel legt fest, wann die Maschine anhält
- Das Problem, allgemein zu entscheiden, ob eine Turing-Maschine irgendwann anhält oder ewig weiterläuft, ist das Halteproblem
- Alan Turing bewies, dass es keine allgemeine Lösung für das Halteproblem gibt
- Die Busy-Beaver-Suche umgeht die allgemeine Lösung für alle Maschinen und klassifiziert stattdessen jede Maschine innerhalb einer endlichen Menge mit fester Regelzahl
Radós Busy Beaver game
- Tibor Radó definierte in einer Arbeit von 1962 das Busy Beaver game, indem er Turing-Maschinen nach ihrer Regelzahl gruppierte
- In der Menge aller Turing-Maschinen mit n Regeln gilt:
- Einige Maschinen laufen ewig
- Einige Maschinen halten an
- Unter den haltenden Maschinen ist die am längsten laufende die Busy Beaver
- Ihre Laufzeit in Schritten ist BB(n)
- Um BB(n) festzulegen, muss man die Laufzeiten aller haltenden Maschinen prüfen und beweisen, dass alle übrigen Maschinen nicht anhalten
- Die Laufzeit lässt sich meist per Computersimulation messen, aber ein Nicht-Halte-Beweis kommt dem Lösen des Halteproblems für eine konkrete Maschine nahe
- Der Busy-Beaver-Challenge-Mitwirkende Shawn Ligocki sieht diese Arbeit als Tätigkeit „an der Grenze des Unbekannten“
Von BB(1) bis BB(4)
- BB(1)=1 lässt sich leicht überprüfen
- Wenn die erste Regel beim Lesen einer 0 das Anhalten vorgibt, stoppt die Maschine im ersten Schritt
- Andernfalls bewegt sie sich einfach weiter über ein mit 0 gefülltes Band
- Schon mit nur 2 Regeln entstehen mehr als 6.000 verschiedene Turing-Maschinen; bei 3 Regeln sind es Millionen, bei 4 Regeln Milliarden
- Allen Brady integrierte einen Genealogie-Ansatz in ein Computerprogramm, um Redundanzen zu verringern, indem Maschinen mit gleichem Anfangsverhalten zusammengefasst wurden
- Shen Lin bewies gemeinsam mit Radó BB(3)=21; das Ergebnis wurde 1965 veröffentlicht
- Brady fand 1966 eine 4-Regel-Maschine, die nach 107 Schritten anhält, und bewies 1974, dass sie BB(4) ist
- BB(4) blieb danach mehr als 40 Jahre lang die letzte Busy-Beaver-Zahl, die der Menschheit bekannt war
Die Jagd nach dem fünften Busy Beaver
- Der Dortmunder Wettbewerb von 1984 war die erste groß angelegte Suche nach BB(5)
- Es gibt fast 17 Billionen Turing-Maschinen mit 5 Regeln; selbst bei einer Auflistung von einer pro Millisekunde würde das mehr als 500 Jahre dauern
- Die beschäftigtste Maschine, die die Dortmunder Teilnehmenden fanden, hielt nach mehr als 100.000 Schritten an
- Später fand ein anderer Forschender eine Maschine, die mehr als 2 Millionen Schritte lief
- Heiner Marxen und Jürgen Buntrock entwickelten mathematische Techniken, um Turing-Maschinen-Simulationen zu beschleunigen
- Marxen ließ 1989 ein Programm über ein Wochenende auf einem leistungsstarken neuen Firmencomputer laufen und fand eine Maschine, die nach 47.176.870 Schritten anhielt
- Buntrock reproduzierte das Ergebnis, und beide veröffentlichten Anfang 1990 eine Arbeit
- Diese Maschine war tatsächlich der fünfte Busy Beaver, aber es dauerte mehr als 30 weitere Jahre, um zu beweisen, dass alle übrigen Maschinen nicht anhalten
Skelet und die ungelösten Maschinen
- Anfang der 2000er-Jahre kam der bulgarische Informatiker Georgi Ivanov Georgiev BB(5) sehr nahe
- Georgiev verbrachte zwei Jahre damit, täglich mehrere Stunden lang sein Programm zur Identifikation nicht haltender Maschinen zu verbessern
- Das fertige Programm bestand aus dichten 6.000 Zeilen Code ohne Kommentare und benötigte über eine Woche Laufzeit
- Das Programm ließ etwa 100 Turing-Maschinen ungelöst zurück, die Georgiev durch manuelle Analyse auf 43 reduzierte
- Georgiev veröffentlichte das Ergebnis 2003 unter dem Pseudonym Skelet online
- Diese 43 schwierigen Maschinen wurden nach seinem Pseudonym als Skelet-Maschinen bekannt
- Georgiev sagte, er sei nach zwei Jahren intensiver Arbeit so erschöpft gewesen, dass ihm keine neuen Ideen mehr kamen
Die kollaborative Struktur der Busy Beaver Challenge
- Tristan Stérin startete 2022 die Busy Beaver Challenge
- Das Projekt war als Online-Kollaboration organisiert und wuchs zu einer internationalen Community von mehr als 20 Personen, darunter viele ohne traditionelle akademische Qualifikationen
- Stérin war überzeugt, dass zur Bestätigung von BB(5) ein dokumentierter und reproduzierbarer Beweis nötig sei
- Georgievs Programm war hochentwickelt, aber für andere Forschende schwer zu prüfen
- Stérin teilte die Arbeit auf Basis bestehender Ansätze auf
- Mit Bradys Genealogie-Ansatz wurden redundante Maschinen entfernt
- Maschinen, die innerhalb von 47.176.870 Schritten anhalten, wurden identifiziert
- Maschinen, die ewig laufen, wurden mit unabhängigen Programmen behandelt, die jeweils eine eigene Beweismethode enthielten
- Ein erstes Programm für die Anfangsphase, Ende 2021 geschrieben, erzeugte eine Liste von etwa 120 Millionen Turing-Maschinen, die zur Bestimmung von BB(5) ausreichte
- Etwa ein Viertel davon hielt früher an als die Maschine von Marxen und Buntrock; 88 Millionen blieben zur weiteren Prüfung übrig
- Stérin baute auch eine Online-Oberfläche mit Raumzeit-Diagrammen, die das Verhalten der Maschinen als zweidimensionales Raster aus 0 und 1 zeigt
Closed Tape Language und beschleunigte Zusammenarbeit
- Shawn Ligocki stieß 2022 zur Busy Beaver Challenge und belebte die von Marxen entwickelte Closed-Tape-Language-Methode wieder
- Diese Methode liefert einen einheitlichen mathematischen Rahmen, um anhand von Mustern auf dem Band einer Turing-Maschine zu zeigen, dass sie nicht anhält
- Ligocki schrieb einen Blogbeitrag, der die Technik vorstellt, wusste aber nicht, wie man ein Programm schreibt, das alle Fälle abdeckt
- Nachdem Justin Blanchard zum Projekt gestoßen war, setzte er dies um, und zwei weitere Mitwirkende steigerten die Ausführungsgeschwindigkeit stark
- Innerhalb weniger Monate wurde die Closed-Tape-Language-Methode zu einem der mächtigsten Werkzeuge des Teams
- Mit dieser Technik ließen sich auch 10 der 43 von Georgiev hinterlassenen Skelet-Maschinen behandeln
- Ligocki meint, dass dieses Ergebnis nicht aus dem Beitrag einer einzelnen Person allein entstanden wäre
Skelet #1, Skelet #17 und Coq
- Skelet #1 war eine Maschine, die zwischen vorhersagbaren und chaotischen Phasen wechselte
- Im März 2023 analysierten Ligocki und Pavel Kropitz Skelet #1, indem sie die 30 Jahre alte beschleunigte Simulationstechnik von Marxen und Buntrock erweiterten
- Skelet #1 trat erst nach mehr als 1 Billion × 1 Billion Schritten in einen Wiederholungszyklus ein, und dieser Zyklus war mit mehr als 8 Milliarden Schritten sehr lang
- Die 21-jährige autodidaktische Programmiererin mei lernte Coq und übersetzte anschließend mehrere Beweise der Busy Beaver Challenge nach Coq
- mei übertrug auch den Nicht-Halte-Beweis von Ligocki und Kropitz für Skelet #1 nach Coq und machte das Ergebnis damit belastbarer
- Skelet #17 war eine weitere schwierige Maschine, bei der Chris Xu der Durchbruch gelang
- Xus Beweis war herausragend, enthielt aber mathematische Intuition, die sich schwer in die von Coq geforderte präzise Form bringen ließ
- Das Team wollte keinen Beweis nach dem Muster „lass das Programm sechs Monate laufen“, sondern einen in vertretbarer Weise reproduzierbaren Beweis
Ein Coq-Beweis mit 40.000 Zeilen
- Im April 2024 stieß ein neuer Mitwirkender, der nur unter dem Pseudonym mxdys bekannt ist, zur Fertigstellung des Coq-Beweises hinzu
- Selbst das Team kennt weder den Aufenthaltsort noch den persönlichen Hintergrund von mxdys
- Am 10. Mai schrieb mxdys auf Discord: „The Coq proof of BB(5) is finished.“
- Innerhalb weniger Wochen integrierte mxdys die Techniken und Ergebnisse der Community und vollendete einen einzigen 40.000 Zeilen umfassenden Coq-Beweis
- Der Beweis ist im Repository Coq-BB5 veröffentlicht
- Der Coq-Experte Yannick Forster von Inria prüfte den Beweis und sagte, die Formalisierung sei alles andere als einfach gewesen
- Damit ist bestätigt, dass die von Marxen und Buntrock vor mehr als 30 Jahren gefundene 47.176.870-Schritte-Maschine tatsächlich der fünfte Busy Beaver ist
- Georgiev sagte, er habe nicht erwartet, dass dieses Problem noch zu seinen Lebzeiten gelöst würde
- Allen Brady starb am 21. April 2024 im Alter von 90 Jahren, einen Monat bevor der Beweis fertiggestellt wurde
BB(6) und die nächste Grenze
- Mitwirkende der Busy Beaver Challenge begannen, eine offizielle wissenschaftliche Arbeit zur Erläuterung des Ergebnisses vorzubereiten
- Die Arbeit soll den Coq-Beweis von mxdys durch für Menschen lesbare Beweise ergänzen
- Einige Teammitglieder wandten sich bereits dem nächsten Busy Beaver zu
- mxdys und Racheline fanden bei BB(6) eine Hürde, die nur schwer zu überwinden scheint
- Diese Hürde ist eine 6-Regel-Maschine mit einem Halteproblem, das der Collatz conjecture ähnelt
- Diese Maschine heißt Antihydra
- Die Verbindung zwischen Turing-Maschinen und der Collatz conjecture reicht bis zu einer Arbeit von Pascal Michel aus dem Jahr 1993 zurück, aber Antihydra scheint die kleinste Maschine zu sein, die sich ohne einen konzeptionellen Durchbruch in der Mathematik nicht lösen lässt
- Scott Aaronson hält es für möglich, dass BB(5) die letzte Busy-Beaver-Zahl ist, die die Menschheit kennen wird
- Einige Mitwirkende wollen sich weiter mit Varianten des Busy-Beaver-Problems befassen, aber nicht alle Beteiligten bleiben in dieselbe Richtung engagiert
- Stérin sagte, die Busy Beaver Challenge habe ihn von der Wirksamkeit online organisierter kollaborativer Forschung überzeugt, und er wolle Software-Werkzeuge entwickeln, die ähnliche Projekte in anderen Bereichen der Mathematik unterstützen
1 Kommentare
Hacker-News-Kommentare
Es gibt einen Kommentar von Scott Aaronson zu diesem Ergebnis: https://scottaaronson.blog/?p=8088
Und es gibt auch große Threads von Anfang dieses Jahres zu „leisure-class beavers“:
https://news.ycombinator.com/item?id=40453221
https://news.ycombinator.com/item?id=38113792
https://news.ycombinator.com/item?id=37910297
Das ursprüngliche Busy-Beaver-Problem hat viele Varianten, und eine davon ist der funktionale Busy Beaver, definiert im Lambda-Kalkül [1]
Da hier die Programmgröße in Bits statt der Anzahl der Zustände gemessen wird, lassen sich mehr Werte bestimmen: Bei Turing-Maschinen ist man bisher erst bei 6, hier dagegen schon bei 37. Der Abstand zwischen dem größten bekannten Wert und Werten jenseits von Graham's Number beträgt außerdem nur 13 Programm-Bits. Eine eng verwandte Variante [2] lässt sich direkt über Kolmogorov-Komplexität ausdrücken, und Mikhail Andreev hält das in [3] für wichtig für Anwendungen der Informationstheorie
[1] https://oeis.org/A333479
[2] https://oeis.org/A361211
[3] https://arxiv.org/pdf/1703.05170
https://oeis.org/A141475 habe ich gefunden, aber dort steht für 5 ein Wert von 27 Billionen
Ich erinnere mich, ein Video gesehen zu haben, das diese Definition erklärt
Ich habe mehrere Jahre mit einem unglaublich smarten und schwer zu begreifenden Ingenieur zusammengearbeitet, der bei einer Elite-Tech-Firma schneller als alle anderen, die ich dort gesehen habe, in den IC-Rängen aufstieg
Er hat das Unternehmen vor einigen Jahren verlassen, und als ich ihn nach seinen Plänen fragte, sagte er, er wolle zum Busy-Beaver-Problem forschen. Ich frage mich, ob der anonyme Mitwirkende mxdys, der laut Artikel den formalen Beweis für BB(5) abgeschlossen hat, diese Person ist, aber vermutlich werde ich es nie erfahren
Ich sehe den Nutzen nicht, und bei einer so außergewöhnlichen Intelligenz hätte ich lieber gesehen, dass sie ein Problem löst, das direkter zur Verbesserung der Welt beiträgt
Tibor Radós ursprüngliche Busy-Beaver-Arbeit „On Non-Computable Functions“ ist tatsächlich ziemlich leicht und unterhaltsam zu lesen
Eine modernisierte Version mit zusätzlichen Anmerkungen gibt es hier: https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Re...
Was hier hervorsticht, ist, dass der Beweis ein Coq-Beweis ist
Ich frage mich, ob dies der erste bedeutende Beweis ist, der von Anfang an in einem Theorembeweiser umgesetzt wurde, statt einen bereits bekannten Beweis nachträglich in einen Assistenten zu übertragen. Es gab zwar schon früher computerunterstützte Beweise, aber der Vierfarbensatz und die Kepler-Vermutung wurden erst später in eine formal verifizierte Umgebung überführt
Das Hauptproblem war, dass die Entscheider und handgeführten Beweise nicht gut organisiert und teilweise etwas fragwürdig waren. Insbesondere brauchte Skelet #1 ein spezialisiertes Programm, um bis zum Endmuster zu beschleunigen [0], und bei Skelet #17 musste Xu sieben dicht gepackte Seiten Argumentation schreiben, um das Nicht-Halten zu beweisen [1]. Der vollständige Coq-Beweis liefert die Vertrauenswürdigkeit, die diese Resultate dringend brauchten
[0] https://www.sligocki.com/2023/03/13/skelet-1-infinite.html
[1] https://discuss.bbchallenge.org/t/skelet-17-does-not-halt/18...
https://github.com/ccz181078/Coq-BB5/blob/main/BB52Theorem.v
https://en.m.wikipedia.org/wiki/Four_color_theorem
Vielleicht habe ich nicht genau verstanden, was mit „formal verifizierter Umgebung“ gemeint ist, aber ich dachte, der Vierfarbensatz sei von Anfang an mit dem Computer bewiesen worden. Kempes ursprünglicher Beweisversuch war fehlerhaft, lieferte aber einige der grundlegenden Werkzeuge, die im späteren Beweis verwendet wurden, und letztlich scheint der Satz per Computer bewiesen worden zu sein
Dieser Busy Beaver wurde 1990 entdeckt, und wahrscheinlich wurden alle Maschinen der Größe 5 kurz danach aufgelistet
Glückwunsch an das Team. Damit ist das Halteproblem für Programme von 5-Zustands-2-Symbol-Turing-Maschinen ausgehend von einem leeren Band nun gewissermaßen gelöst.
Ich frage mich, ob jemand dieselbe Technik schon auf den Fall mit 2 Zuständen und 4 Symbolen angewandt hat. Im Allgemeinen sind Symbole zwar mächtiger als Zustände, aber das scheint noch handhabbar zu sein, und vielleicht kämen dabei auch unerwartete Ergebnisse heraus. 6 Zustände mit 2 Symbolen und 2 Zustände mit 5 Symbolen wirken beide schwer zu behandeln, vielleicht sogar in beweisbarer Weise schwer. Nebenbei gibt es die absurde, aber seltsam weit verbreitete Vorstellung, Menschen könnten mit dem geistigen Auge oder mit Quantenmechanik im Gehirn intuitiv Lösungen für das Halteproblem erfassen; natürlich spielte so etwas in diesem Beweis keine Rolle.
Soweit ich weiß, reicht schon der derzeit verwendete Decider aus, um zu beweisen, dass alle verbleibenden 2×4-Fälle nicht haltend sind. Wenn es also keinen großen Fehler im Entwurf des Deciders gibt, erhält man aus dem aktuellen Champion Σ(2,4) = 2,050 und S(2,4) = 3,932,964. Die Resultate sind nur noch nicht an einer Stelle zusammengefasst.
Für 2×5 gibt es Hydra und für 6×2 Antihydra; beide berechnen dieselbe Iteration, nur mit unterschiedlichen Startpunkten und Haltebedingungen. Die Standardvermutung ist, dass diese Iteration im Zusammenhang mit Mahler’s 3/2 problem modulo 2 gleichverteilt ist, und ein Beweis dieser Vermutung würde obere und untere Schranken für das kumulierte Verhältnis von 0 und 1 liefern, womit sich das Nichthalten der beiden Maschinen mit hoher Wahrscheinlichkeit beweisen ließe. Natürlich gibt es dafür keine bekannte Beweismethode.
Dazu wurde ein auf einer logischen Theorie basierender Beweisgenerator namens Aleph* verwendet, und damals war bereits seit 1.500 Jahren bekannt, dass ZFC BB(18) nicht beweisen kann. Verglichen mit 2024 hätte kein Programm aus der Zeit lange vor Aleph* selbst theoretisch für brute-forceartige Beweisprüfung eingesetzt werden können, um BB(18) zu lösen. Das steht im Gegensatz dazu, dass wir heute durch Aufzählen und Prüfen von ZFC-Beweisen theoretisch BB(??) lösen könnten.
Die Position „Menschen intuitieren Lösungen des Halteproblems“ bedeutet so etwas. Soweit ich weiß, gibt es keinen starken theoretischen Grund, warum eine solche Zukunftsgeschichte unmöglich sein sollte. Und weil der Busy Beaver nicht berechenbar ist, hätten Menschen neue Theorien entwickeln müssen, um das nötige Programm zu erstellen. Irgendetwas muss die Anerkennung für das Ergebnis bekommen, und da das Programm damals noch nicht existierte, kann sie nicht an die Berechnung gehen.
Ich frage mich, ob es einfach ein Zufall war, dass sich für alle nicht haltenden Programme der Länge 5 auch beweisen ließ, dass sie nicht halten.
„Die Tatsache, dass Σ(5) = 1,915 und S(5) = 2,358,064, wird niemals bewiesen werden. Oder falls eine größere untere Schranke gefunden wird, setzen Sie einfach diesen neuen Wert in diese Vorhersage ein.“
Der Grund war, dass die Natur sehr wahrscheinlich unter den noch offenen 5-Zustands-Maschinen mindestens ein Problem versteckt haben könnte, das so schwer zu fassen ist wie die Goldbachsche Vermutung. Anders gesagt: Es schien gut möglich, dass es rekursive Nichthalte-Muster gibt, die über unsere kognitive Erkennungsfähigkeit hinausgehen. Zum Glück wurde diese Vorhersage nicht Realität, aber es war nur ein zusätzlicher Zustand Unterschied.
[0] Allen Brady, "The Busy Beaver Game and the Meaning of Life", in Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey, Oxford University Press, 1988, pp. 259–277. This chapter can also be found in the 2nd ed., Springer, 1995, pp. 237–254.
Im praktischen Sinn haben andere darauf schon geantwortet. Im mathematischen Sinn wäre es ziemlich überraschend gewesen, wenn BB(5) unentscheidbar gewesen wäre. 5 Zustände und 2 Symbole sind einfach zu klein, um unentscheidbares Verhalten zu kodieren.
Aufgrund der Unvollständigkeitssätze muss es allerdings ein n geben, für das die Standardmathematik den Wert von BB(n) nicht beweisen kann. In den letzten Jahren haben mehrere Leute untersucht, wie klein man ein solches n machen kann, und der aktuelle Rekord[0] liegt bei 745. Dieser Rekord lässt sich vermutlich noch senken, trotzdem bleibt eine große Lücke zwischen dem größten Wert, den wir kennen, nämlich 5, und dem kleinsten Wert, von dem wir wissen, dass er unbekannt sein kann, nämlich 745.
[0] Falls sich jemand fragt, was mit „Standardmathematik“ gemeint ist: Das ist der aktuelle Rekord sowohl für ZFC als auch für PA. Also sollte sich der Wert zumindest für PA weiter senken lassen. Bisher scheint nur noch niemand einen besseren Ansatz als für ZFC gefunden zu haben, aber eigentlich sollte das doch möglich sein, oder?
„Vor nur vier Tagen entdeckten mxdys und Racheline, zwei weitere Beitragende, für BB(6) eine Hürde, die schwer zu überwinden scheint: eine 6-Regeln-Maschine, deren Halteproblem dem notorisch schwierigen mathematischen Problem der Collatz-Vermutung ähnelt. Die Verbindung zwischen Turing-Maschinen und der Collatz-Vermutung reicht bis zu einer Arbeit des Mathematikers Pascal Michel aus dem Jahr 1993 zurück, aber die neu entdeckte Maschine namens ‚Antihydra‘ scheint die kleinste Maschine zu sein, die sich ohne einen konzeptionellen Durchbruch in der Mathematik nicht lösen lässt.“
Ich habe als Privatprojekt einmal ein Programm geschrieben, das das Cutting-stock-Problem (https://en.wikipedia.org/wiki/Cutting_stock_problem) löst.
Zum Bestand gehörten zugeschnittene Stücke in den Formen /---/, /---| und |---|, und ich konnte oder wollte kein vorhandenes Programm verwenden, weil ich bei 45-Grad-Schnitten kein Material verschwenden wollte. Die Erklärung, dass Brady zur Optimierung der BB(4)-Suche Teilbäume des Suchraums abgeschnitten hat, in denen Unterschiede keine Rolle spielten, fand ich interessant, weil das ziemlich ähnlich zu dem war, was ich getan habe, um mein Programm schnell zu machen.
Laut einem Blogbeitrag von Scott Aaronson gibt es 16,679,880,978,201 5-Zustands-Turing-Maschinen.
Ich frage mich, ob bekannt ist, wie viel Prozent davon halten. Korrektur: Die Anzahl der Turing-Maschinen mit n Zuständen ist (4n + 1)^(2n). Ich habe Material für kleine n gefunden, das der Analyse ähnelt, nach der ich gesucht habe: https://github.com/LukasKalbertodt/beaver
Auf bbchallenge.org habe ich ihn nicht gefunden, aber alle Maschinen sind klassifiziert.
Insgesamt ist der Beweis ziemlich kurz. Einschließlich Leerzeichen und Kommentaren umfasst er 19.000 Zeilen Coq
Meiner Erfahrung nach würde er, in eine traditionelle wissenschaftliche Arbeit kompiliert, deutlich kürzer ausfallen als die Coq-Version. Natürlich ist die Länge eines Beweises kein Maß für Schwierigkeit oder Komplexität, aber als sehr grober Maßstab kann sie dienen
Wenn es um die Grenzen menschlichen Wissens geht, denkt man oft an Sätze, die zwar beweisbar sind, aber so komplex, dass kein Mensch sie verstehen kann. Der wohl komplexeste Beweis, den wir haben, ist die Klassifikation der endlichen einfachen Gruppen; sie umfasst Zehn- oder Hunderttausende Seiten, und es gibt wahrscheinlich nur sehr wenige oder vielleicht gar keine Menschen auf der Erde, die sie vollständig verstehen
Wie im Artikel gesagt, könnte BB(6) unentscheidbar sein. Es könnte aber auch sein, dass es einen Beweis mit Millionen von Seiten gibt, der außerhalb der Reichweite der Menschheit liegt