💻 computer science

Determination of the fifth Busy Beaver value

De auteurs hebben met behulp van de Coq-bewijshulp het vijfde Busy Beaver-getal voor het eerst in meer dan 40 jaar vastgesteld en formeel geverifieerd als 47.176.870 door 181.385.789 Turing-machines te analyseren.

Oorspronkelijke auteurs: The bbchallenge Collaboration, Justin Blanchard, Daniel Briggs, Konrad Deka, Nathan Fenner, Yannick Forster, Georgi Georgiev, Matthew L. House, Rachel Hunter, Iijil, Maja Kądziołka, Pavel Kropitz, Sha

Gepubliceerd 2026-03-24

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: The bbchallenge Collaboration, Justin Blanchard, Daniel Briggs, Konrad Deka, Nathan Fenner, Yannick Forster, Georgi Georgiev, Matthew L. House, Rachel Hunter, Iijil, Maja Kądziołka, Pavel Kropitz, Shawn Ligocki, mxdys, Mateusz Naściszewski, savask, Tristan Stérin, Chris Xu, Jason Yuen, Théo Zimmermann

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een enorme, oneindige stripboekpagina hebt. Op deze pagina staat een heel simpel spelletje: je hebt een kleine robot (een Turing-machine) en een lange rol papier met alleen maar nullen erop. De robot heeft een beperkt aantal "hersenen" (states) en moet een reeks simpele instructies volgen.

Het doel van dit spel is tweeledig:

Hoe lang kan de robot lopen voordat hij stopt? (Dit noemen we $S(n)$ ).
Hoeveel '1'-jes kan hij op zijn papier schrijven voordat hij stopt? (Dit noemen we $\Sigma(n)$ ).

Deze robots zijn zo simpel dat je zou denken dat we ze allemaal makkelijk kunnen begrijpen. Maar hier zit de twist: voor een groot aantal robots is het onmogelijk om te voorspellen of ze ooit stoppen of dat ze voor eeuwig blijven doordraaien. Dit is het beroemde "Halting Problem".

Dit artikel vertelt het verhaal van een gigantisch, wereldwijd team van vrijwilligers (de bbchallenge Collaboration) dat eindelijk het antwoord heeft gevonden voor robots met 5 hersenen.

De Grote Uitdaging: De "Busy Beaver"

De winnaar van dit spel voor een bepaald aantal hersenen heet de "Busy Beaver" (Bezigste Bevers). Voor 5 hersenen wisten we al sinds 1989 dat er een robot was die 47.176.870 stappen kon zetten. Maar niemand wist zeker of er niet nog een andere, slimmere robot bestond die nog langer kon lopen.

Het probleem is dat er 181 miljoen verschillende robots met 5 hersenen zijn. Als je ze één voor één zou testen, zou het duizenden jaren duren. En sommige robots lopen zo lang dat ze pas stoppen na een aantal stappen dat groter is dan het aantal atomen in het heelal.

De Oplossing: Een Digitale Gids en een Wiskundig Bewijs

Het team heeft dit opgelost met twee slimme trucs:

1. De "Boom" van de Robots (Tree Normal Form)
In plaats van alle 181 miljoen robots willekeurig te testen, hebben ze ze georganiseerd in een gigantische boomstructuur.

Analogie: Stel je voor dat je alle mogelijke gezinnen wilt vinden. In plaats van elk huis in de stad af te lopen, bouw je een stamboom. Je begint bij de wortel (geen instructies) en groeit takken uit. Als een tak al "dood" is (de robot stopt direct of loopt in een cirkel), hoef je die tak niet verder te verkennen.
Door slimme wiskundige regels toe te passen, hebben ze de zoekruimte teruggebracht van 16 biljoen naar "slechts" 181 miljoen. Dat is nog steeds veel, maar haalbaar voor computers.

2. De "Detective-Team" (Deciders)
Ze hebben geen enkele robot handmatig gecontroleerd. In plaats daarvan hebben ze een reeks slimme algoritmes (detectives) gebouwd.

Analogie: Stel je voor dat je een huis wilt controleren op inbrekers. Je hebt niet één agent nodig die alles ziet, maar een team:
- De Loop-Detective kijkt of de robot in een cirkel loopt (zoals een hond die achter zijn staart jaagt).
- De Patroon-Detective kijkt of de robot een herhalend patroon maakt, zoals een fractal of een telmachine.
- De Automatische Vertaler vertaalt de robot naar een eenvoudiger systeem om te zien of hij vastloopt.
Deze detectives hebben 99,9% van de robots snel afgehandeld. Ze konden bewijzen: "Deze robot stopt na 100 stappen" of "Deze robot loopt oneindig door".

3. De "Lastige Buren" (Sporadic Machines)
Er bleven 13 robots over die zo raar en complex waren dat de detectives ze niet konden oplossen. Deze noemen ze "Sporadische Machines".

Analogie: Dit zijn de buren die een heel raar huis hebben, met trappen die naar de lucht leiden en deuren die naar binnen leiden. De standaard detectives konden hier niet bij.
Voor deze 13 robots hebben wiskunden individuele, zeer complexe bewijzen moeten schrijven. Een van deze robots (Skelet #1) loopt bijvoorbeeld pas na 541 duizend miljard miljard miljard stappen in een cirkel. Dat is langer dan de leeftijd van het heelal!

Het Grote Bewijs: De "Coq"

Om zeker te zijn dat ze geen fouten hadden gemaakt, gebruikten ze een computerprogramma genaamd Coq.

Analogie: Stel je voor dat je een heel lang wiskundig betoog schrijft. Normaal leest een mens het na. Maar als het betoog 181 miljoen regels lang is, kan een mens dat niet controleren.
Coq is een "super-rekenmachine" die elke stap van het bewijs controleert. Het zegt: "Ja, dit is logisch. En dit ook. En dit ook." Als Coq zegt "OK", dan is het een feit.
Dit is het eerste keer in de geschiedenis dat een Busy Beaver-waarde volledig door een computer is geverifieerd.

Het Resultaat

Het team heeft bewezen dat:

De langst lopende robot met 5 hersenen precies 47.176.870 stappen maakt.
Er geen enkele andere robot is die langer loopt.
De winnaar is de robot die in 1989 al gevonden was (door Marxen en Buntrock), maar nu weten we het zeker.

Waarom is dit belangrijk?

Dit is meer dan alleen een spelletje.

De grens van kennis: Het laat zien waar onze kennis ophoudt. Voor 6 hersenen zijn er robots die zo complex zijn dat ze waarschijnlijk nooit opgelost kunnen worden met huidige wiskunde. Ze zijn als "cryptiden" (zoals de Bigfoot van de wiskunde): we vermoeden dat ze bestaan, maar we kunnen ze niet bewijzen.
Samenwerking: Dit project toont aan dat als duizenden mensen (studenten, programmeurs, wiskundigen) online samenwerken, ze problemen kunnen oplossen die voor één persoon onmogelijk zijn.
AI en Toekomst: Het is een test voor kunstmatige intelligentie. Als AI-systemen in de toekomst dit soort complexe bewijzen kunnen vinden, dan kunnen ze misschien de "onoplosbare" problemen van de wiskunde kraken.

Kortom: Een wereldwijd team heeft met de hulp van slimme computers en een digitale "super-rekenmachine" bewezen dat de snelste 5-staps robot precies 47 miljoen stappen zet. Het is een overwinning voor de menselijke nieuwsgierigheid en samenwerking.

Titel: Bepaling van de vijfde Busy Beaver-waarde

Auteurs: De bbchallenge Collaboration (o.a. Justin Blanchard, Daniel Briggs, Pavel Kropitz, mxdys, Tristan Stérin, Théo Zimmermann, etc.)

1. Het Probleem: De Busy Beaver-functie

De paper behandelt het "Busy Beaver"-spel, geïntroduceerd door Tibor Radó in 1962. Het doel is om de maximale stapwaarde $S(n)$ te bepalen voor een Turingmachine met $n$ toestanden en 2 symbolen (0 en 1), die start met een volledig met nullen gevulde tape en uiteindelijk stopt.

Onberekenbaarheid: $S(n)$ is een onberekenbare functie. Als $S(n)$ bekend zou zijn, zou het stopprobleem voor Turingmachines oplosbaar zijn, wat onmogelijk is.
Historische context: Voor deze publicatie waren slechts de eerste vier waarden bewezen: $S(1)=1$ , $S(2)=6$ , $S(3)=21$ , en $S(4)=107$ .
De uitdaging: Sinds 1989 was er een kandidaat voor $S(5)$ die 47.176.870 stappen maakte (ontdekt door Marxen en Buntrock), maar het was nooit formeel bewezen dat er geen andere 5-toestandsmachine meer stappen kon maken. Het bewijzen dat een machine niet stopt is extreem moeilijk, aangezien dit wiskundige stellingen (zoals de Goudsbob-conjectuur) kan impliceren die onafhankelijk van de axioma's van ZF (Zermelo-Fraenkel) kunnen zijn.

2. Methodologie

De auteurs hebben een hybride aanpak gebruikt die samenwerking, geavanceerde algoritmen en formele verificatie combineert.

A. De bbchallenge Collaboratie

Sinds 2022 heeft een grote online gemeenschap (bbchallenge.org) samengewerkt om het probleem op te lossen. Duizenden vrijwilligers hebben deciders (algoritmen die bepalen of een machine stopt of niet) ontwikkeld in diverse programmeertalen.

B. Boom-vormige Normalisatie (Tree Normal Form - TNF)

Om de zoekruimte beheersbaar te maken, gebruiken de auteurs de TNF-methode (geïntroduceerd door Brady in 1963).

In plaats van alle $1,67 \times 10^{13}$ syntactische 5-toestandsmachines te testen, reduceert TNF dit tot 181.385.789 unieke machines.
Dit wordt gedaan door machines recursief op te bouwen en irrelevante toestanden/symbolen (die nooit bereikt worden) en permutaties (die identiek zijn door hernoeming) uit te sluiten.

C. Deciders en de "Pipeline"

Elk van de 181 miljoen machines wordt door een "pipeline" van deciders gevoerd. Een decider is een algoritme dat probeert te bewijzen dat een machine stopt (HALT) of niet stopt (NONHALT). Als geen enkel decider een antwoord geeft, blijft de machine een "holdout".
De belangrijkste deciders in de Coq-BB5 pipeline zijn:

Loops: Detecteert cycli en getranslateerde cycli (waarbij het patroon zich herhaalt maar verschoven is op het tape). Dit lost 95,48% van de niet-stoptende machines op.
NGramCPS (n-gram Closed Position Set): Een techniek die lokale configuraties (toestand + n-grammen links/rechts van het hoofd) analyseert om te bewijzen dat een machine in een gesloten verzameling van niet-stoptende toestanden blijft. Dit lost 99,89% van de resterende niet-stoptende machines op.
RepWL (Repeated Word List): Gebruikt reguliere expressies om herhalende patronen op het tape te detecteren.
FAR (Finite Automata Reduction) & WFAR (Weighted FAR): Gebruiken eindige automaten (en gewogen automaten) om een "co-CTL" (Closed Tape Language) bewijs te leveren dat de machine niet stopt.
Sporadische Machines: Voor 13 specifieke machines die door geen enkel decider opgelost konden worden, zijn individuele, handgeschreven wiskundige bewijzen in Coq opgesteld.

D. Formele Verificatie met Coq

Het meest cruciale aspect is dat het volledige bewijs is geïmplementeerd en geverifieerd met Coq, een interactief bewijshulpmiddel.

Coq-BB5: Een Coq-project dat de TNF-enumeratie, alle deciders en de individuele bewijzen voor de sporadische machines bevat.
Reflectie: Het bewijs voert de berekeningen (enumeratie en decider-logica) zelf uit binnen Coq en gebruikt de geverifieerde output om het resultaat te concluderen.
Validatie: De broncode is openbaar, en de compilatie duurt ongeveer 45 minuten op 13 kernen. Het bewijs vertrouwt slechts op één standaardaxioma (functional_extensionality_dep).

3. Belangrijkste Resultaten

$S(5) = 47.176.870$ : Het paper bewijst formeel dat de maximale stapwaarde voor 5-toestandsmachines 47.176.870 is. De winnende machine is dezelfde die in 1989 door Marxen en Buntrock werd gevonden.
$\Sigma(5) = 4.098$ : Het bewijst ook het maximale aantal enen op de tape bij het stoppen.
$S(2, 4) = 3.932.964$ : Een nieuw bewijs voor de Busy Beaver-waarde van machines met 2 toestanden en 4 symbolen.
Bevestiging van $S(4)$ : Het bevestigt de waarde $S(4) = 107$ , wat eerder door Brady was bewezen maar met minder strikte formele verificatie.
Data: De volledige lijst van alle 181.385.789 geverifieerde machines, hun stopstatus en de gebruikte decider, is openbaar beschikbaar gesteld.

4. Bijzondere Vondsten: "Sporadische Machines"

Twaalf van de dertien machines die individuele bewijzen vereisten, waren al bekend als "holdouts" van eerdere pogingen (o.a. van Georgi Georgiev, alias "Skelet"). Deze machines vertonen complexe, niet-triviale gedragingen:

Skelet #1: Een getranslateerde cyclus met een pre-periode van ongeveer $5,41 \times 10^{51}$ stappen en een periode van 8,4 miljard stappen.
Skelet #10: Implementeert twee onafhankelijke "Fibonacci-tellers" (in basis Fibonacci).
Skelet #17: De "final boss". Deze machine beheert een lijst van gehele getallen in een Gray-code-achtige transformatie. Het bewijs dat deze niet stopt, was het laatste stukje dat nodig was voor de volledige oplossing.

5. Betekenis en Impact

Eerste formeel geverifieerde Busy Beaver-waarde: Dit is het eerste keer dat een nieuwe Busy Beaver-waarde niet alleen berekend, maar ook formeel wiskundig bewezen is met een proof assistant. Dit elimineert de twijfel over de juistheid van eerdere handmatige of semi-automatische resultaten.
Grootste samenwerking: Het project demonstreert de kracht van "massively collaborative online research". Duizenden mensen, vaak zonder academische achtergrond, hebben bijgedragen aan een wiskundig probleem van wereldklasse.
Grenzen van wiskundige kennis: Het paper illustreert dat $S(5)$ het kleinste open probleem is dat niet voortkomt uit 5-toestandsmachines. De volgende uitdagingen ( $S(6)$ ) bevatten "Cryptids" (machines waarvan het stopprobleem waarschijnlijk onoplosbaar is binnen standaard axioma's zoals ZF, vergelijkbaar met de Collatz-conjectuur).
AI en Proof Assistants: Het project toont aan hoe proof assistants (Coq) en AI (die getest is op het bewijzen van de eerste lemmata) samenwerken om complexe wiskundige problemen op te lossen. Het bewijs is een "proof by reflection", waarbij de computer de berekening uitvoert en het bewijs dat de berekening correct is, levert.

Conclusie:
Dit paper markeert een mijlpaal in de theoretische informatica. Het lost een probleem op dat meer dan 40 jaar open stond, bewijst dat de huidige kampioen voor 5-toestandsmachines de echte winnaar is, en doet dit op een manier die volledig reproduceerbaar en formeel verifieerbaar is. Het opent de weg voor het bestuderen van nog complexere machines ( $S(6)$ ), waarbij de grenzen van wat wiskundig bewijsbaar is, duidelijk worden getoond.