💻 computer science

Determination of the fifth Busy Beaver value

Cet article présente la preuve formelle, effectuée avec l'assistant Coq, que la valeur de la fonction Busy Beaver pour 5 états est égale à 47 176 870, marquant la première détermination vérifiée d'une nouvelle valeur de cette fonction en plus de 40 ans grâce à une recherche collaborative en ligne.

Auteurs originaux : 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

Publié 2026-03-24

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : 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

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous avez une machine à écrire magique, mais avec une règle très simple : elle ne peut écrire que des zéros et des uns, et elle a un nombre limité de "boutons" (des états) pour décider quoi faire à chaque instant.

C'est ce qu'on appelle une Machine de Turing.

Maintenant, posez-vous cette question : Quelle est la machine la plus "têtue" possible ? C'est-à-dire, quelle machine peut écrire le plus grand nombre de "1" sur sa bande de papier avant de s'arrêter, si on lui donne une bande vierge (toute en zéros) ?

C'est le jeu du Busy Beaver (le "Castor Occupé"). Plus vous ajoutez de boutons (d'états) à votre machine, plus le nombre de "1" qu'elle peut écrire devient astronomique, et plus il est difficile de prédire quand elle va s'arrêter. En fait, pour un nombre d'états assez grand, c'est mathématiquement impossible de le savoir. C'est un problème "incomputable".

Le Grand Défi : Le Cas des 5 Boutons

Pendant des décennies, les mathématiciens savaient exactement combien de "1" pouvaient écrire les machines avec 1, 2, 3 ou 4 boutons. Mais pour 5 boutons, le mystère durait depuis 40 ans !

On savait qu'une machine trouvée en 1989 par deux chercheurs (Marxen et Buntrock) pouvait écrire 47 176 870 uns avant de s'arrêter. C'était le record. Mais personne ne pouvait prouver qu'il n'existait pas une autre machine, encore plus têtue, capable de faire mieux.

Ce papier annonce la fin du mystère :
Grâce à un travail colossal et collaboratif, une équipe internationale a prouvé, à l'aide d'un logiciel de vérification mathématique appelé Coq, que la machine de 1989 est bien la championne. Il n'y a pas de machine à 5 boutons qui peut faire plus de 47 176 870 pas.

Comment ont-ils fait ? (L'Analogie de la Forêt)

Imaginez qu'il existe 16 000 milliards de machines différentes à 5 boutons. C'est une forêt immense. Si vous essayez de les tester une par une, vous ne finirez jamais.

L'équipe a utilisé une astuce géniale pour réduire cette forêt à une simple allée de 181 millions de sentiers (grâce à une méthode appelée "Forme Normale Arborescente"). C'est déjà énorme, mais gérable pour un ordinateur moderne.

Ensuite, ils ont construit une usine de tri (un "pipeline") pour examiner chaque machine :

Le Détecteur de Boucles (Loops) : La plupart des machines qui ne s'arrêtent pas finissent par tourner en rond, comme un hamster sur sa roue. L'ordinateur a repéré et éliminé 95 % des machines "perdues" en détectant ces boucles presque instantanément.
Les Experts (NGramCPS, RepWL, etc.) : Pour les machines plus subtiles qui ne tournent pas en rond immédiatement, l'équipe a créé des détecteurs spécialisés. C'est comme si vous aviez un détective pour les voleurs de banque, un autre pour les espions, et un autre pour les cambrioleurs discrets. Ces "détecteurs" ont résolu 99,9 % des cas restants.
Les Cas Spéciaux (Les "Sporadiques") : Il restait 13 machines très bizarres, des "monstres" qui ne rentrent dans aucune catégorie. Elles ont des comportements incroyables :
- L'une d'elles tourne en rond après 54 000 000 000 000 000 000 000 000 000 000 000 000 000 000 000 000 de pas ! (C'est plus long que l'âge de l'univers).
- Une autre compte en utilisant la suite de Fibonacci (1, 2, 3, 5, 8...) sur deux bandes séparées.
- Pour ces 13 cas, les humains ont dû écrire des preuves mathématiques manuelles, très complexes, puis les ont données à l'ordinateur pour qu'il les vérifie ligne par ligne.

La Collaboration : Une Armée de Volontaires

Ce qui rend ce résultat unique, c'est comment il a été obtenu. Ce n'est pas le travail d'un seul génie isolé dans un bureau. C'est le fruit d'une collaboration massive en ligne, appelée bbchallenge.org.

Des centaines de personnes, de tous âges et de tous pays (étudiants, développeurs, amateurs), se sont réunies sur un serveur de discussion (Discord) pour :

Inventer de nouveaux détecteurs.
Vérifier les preuves.
Discuter des comportements étranges de ces machines.

C'est comme si des milliers d'architectes avaient collaboré pour construire un pont, chacun apportant sa pierre, sans savoir qui était le chef.

Pourquoi est-ce important ?

La Preuve Absolue : C'est la première fois qu'un nombre de Busy Beaver est prouvé avec une certitude mathématique absolue, vérifiée par un logiciel. Pas de "je pense que c'est vrai", mais "c'est mathématiquement certain".
La Frontière de la Connaissance : Cela nous dit où s'arrête notre capacité à comprendre les algorithmes simples. Pour 5 boutons, on y est arrivé. Pour 6 boutons ? C'est probablement impossible. Il existe des machines à 6 boutons dont le comportement est lié à des problèmes mathématiques non résolus (comme la conjecture de Collatz). Si on ne peut pas résoudre ces conjectures, on ne pourra jamais savoir si ces machines s'arrêtent ou non.
L'Intelligence Artificielle : Ce projet sert aussi de banc d'essai pour l'IA. Les chercheurs testent des IA pour voir si elles peuvent aider à prouver ces théorèmes. Pour l'instant, elles réussissent environ la moitié des petits défis, mais le chemin est encore long.

En Résumé

Ce papier est le récit d'une chasse au trésor mathématique. L'équipe a parcouru une forêt de 181 millions de machines, a éliminé les fausses pistes avec des détecteurs ingénieux, et a prouvé que le trésor (le record de 47 millions de pas) est bien celui qu'on pensait. C'est une victoire de la collaboration humaine, de la rigueur informatique et de la curiosité scientifique.

Et la prochaine étape ? Probablement impossible. Car pour 6 boutons, le jeu devient un labyrinthe où les murs sont faits de problèmes mathématiques que nous ne savons pas encore résoudre.

1. Le Problème : La Fonction de Busy Beaver

L'article traite de la détermination de la valeur de la fonction $S(n)$ , définie par Tibor Radó en 1962. $S(n)$ représente le nombre maximal d'étapes qu'une machine de Turing à $n$ états et 2 symboles peut effectuer en partant d'un ruban entièrement vide (tous 0) avant de s'arrêter.

Nature du problème : $S(n)$ est une fonction non calculable. Si elle l'était, elle permettrait de résoudre le problème de l'arrêt de Turing.
Contexte historique : Avant ce travail, seules les quatre premières valeurs étaient prouvées : $S(1)=1$ , $S(2)=6$ , $S(3)=21$ , et $S(4)=107$ . La valeur de $S(5)$ était conjecturée depuis 1989 (par Marxen et Buntrock) être égale à 47 176 870, mais aucune preuve formelle n'existait pour confirmer qu'aucune autre machine à 5 états ne pouvait dépasser ce nombre d'étapes.

2. Méthodologie et Approche

L'équipe bbchallenge Collaboration a résolu ce problème en combinant une recherche collaborative massive et une vérification formelle rigoureuse utilisant l'assistant de preuves Coq.

A. Énumération via la Forme Normale Arborescente (TNF)

Pour réduire l'espace de recherche colossal (environ $1,67 \times 10^{13}$ machines syntactiquement possibles pour $n=5$ ), les auteurs utilisent la Tree Normal Form (TNF).

Cette méthode élimine les transitions inaccessibles et les permutations redondantes d'états/symboles.
Le nombre de machines à analyser est réduit à 181 385 789.
L'énumération est elle-même implémentée et exécutée directement dans Coq, garantissant qu'aucune machine n'est oubliée.

B. Pipeline de Décideurs (Deciders)

Puisque le problème de l'arrêt est indécidable, il n'existe pas de décideur universel. L'équipe a développé un pipeline de plusieurs algorithmes (décideurs) basés sur le cadre Closed Tape Language (CTL) (Langage de Ruban Fermé). Ce cadre approxime l'ensemble des configurations visitées par une machine par un sur-ensemble régulier (ou pondéré) qui ne contient aucune configuration d'arrêt.
Les décideurs principaux utilisés sont :

Loops (Boucles) : Détecte les cycles simples et les "Translated Cyclers" (cycles décalés dans l'espace) en analysant l'historique des états et positions sans simuler le contenu complet du ruban.
NGramCPS (n-gram Closed Position Set) : Une simplification de la technique CPS, utilisant des n-grammes (séquences de symboles) et des augmentations de l'alphabet (historique fixe ou LRU) pour prouver la non-termination.
RepWL (Repeated Word List) : Utilise des expressions régulières pour modéliser des blocs de symboles répétés sur le ruban.
FAR (Finite Automata Reduction) : Une technique de co-CTL utilisant des Automates Finis Non Déterministes (NFA) pour prouver que les configurations d'arrêt ne sont pas atteignables.
WFAR (Weighted FAR) : Une généralisation de FAR utilisant des automates pondérés pour gérer des configurations non régulières complexes.

C. Machines Sporadiques

Pour 13 machines spécifiques (appelées "Sporadic Machines") qui résistaient à tous les décideurs automatisés, l'équipe a fourni des preuves individuelles de non-arrêt formalisées dans Coq. Ces machines présentent des comportements complexes (compteurs de Fibonacci doubles, codes Gray obscurcis, cycles avec des pré-périodes gigantesques de l'ordre de $10^{51}$ ).

3. Résultats Principaux

Théorème 1.1 : $S(5) = 47\,176\,870$ .
- La preuve a été formalisée dans le projet Coq-BB5.
- Elle confirme que la machine découverte par Marxen et Buntrock en 1989 est bien le champion absolu pour 5 états.
- Le résultat est le premier déterminé depuis plus de 40 ans et le premier à être formellement vérifié.
Théorème 1.2 : $S(2, 4) = 3\,932\,964$ .
- Détermination de la valeur maximale pour les machines à 2 états et 4 symboles.
Autres résultats :
- Confirmation de $S(4) = 107$ .
- Calcul de $\Sigma(5) = 4\,098$ (le nombre maximal de 1 sur le ruban à l'arrêt).
- Calcul de $space(5) = 12\,289$ (nombre maximal de cellules visitées).

4. Contributions Techniques et Innovations

Vérification Formelle à Grande Échelle : C'est l'un des premiers exemples où l'énumération de centaines de millions d'objets (machines de Turing) et leur analyse sont entièrement intégrées dans un assistant de preuves (Coq). Cela élimine tout risque d'erreur humaine ou de bug logiciel dans la logique de décision.
Collaboration Ouverte (bbchallenge.org) : Le projet a réuni des centaines de contributeurs (amateurs et professionnels) via un serveur Discord et un wiki. L'approche "build in public" a permis de développer des décideurs dans de nombreux langages (C++, Rust, Python, Haskell, Coq, etc.) avant leur intégration finale.
Nouveaux Algorithmes : Développement de décideurs originaux (Loops, NGramCPS, WFAR) capables de résoudre plus de 99,99 % des machines halting et 99,89 % des machines non-halting (hors boucles simples) pour $n=5$ .
Zoologie des Machines : L'analyse a permis de classifier les machines en familles comportementales (Bouncers, Counters, Fractals, Helices, etc.), offrant une meilleure compréhension de la "faune" algorithmique des machines de Turing.

5. Signification et Impact

Preuve de Concept pour la Recherche Collaborative : L'article démontre l'efficacité d'une recherche scientifique massive, décentralisée et ouverte, où la confiance est établie par la reproductibilité et la vérification formelle plutôt que par la réputation des auteurs.
Limites de la Connaissabilité Mathématique : L'étude met en lumière la frontière entre le calculable et l'inconnaissable. Bien que $S(5)$ soit résolu, l'article identifie des "Cryptids" (machines dont le problème d'arrêt est mathématiquement difficile, lié à des conjectures comme celle de Collatz) pour $n=6$ , suggérant que $S(6)$ pourrait être impossible à prouver dans les systèmes axiomatiques standards (comme ZF).
Benchmark pour l'IA : La complexité de ces problèmes (notamment les preuves pour les machines sporadiques) sert de banc d'essai pour les systèmes d'intelligence artificielle, qui ont déjà été testés sur les premières lemmes de cette preuve avec un taux de succès partiel.

En résumé, ce travail marque une étape historique en informatique théorique en résolvant un problème ouvert depuis des décennies grâce à une synergie entre l'intelligence humaine distribuée et la rigueur des assistants de preuve formels.