Jeu Du Castor Occupé

Le jeu du castor occupé est un problème informatique théorique proposé en 1962 par le mathématicien Tibor Radó. Le jeu implique un type spécial de machine de Turing appelée « castor occupé », qui est un programme conçu pour écrire autant de « 1 » que possible sur un morceau de papier infiniment long. Dans le jeu Busy Beaver, étant donné un entier positif, considérez toutes les machines de Turing avec des états (y compris l'alphabet d'entrée et la fonction de transition d'état, etc.). Le but du jeu est de trouver une machine de Turing qui, étant donné une entrée vide, prend le plus de temps (ou le plus d'étapes) avant de s'arrêter, tout en produisant le plus grand nombre de 1. Le nombre de 1 dans cette sortie est la valeur de la fonction de castor occupé correspondant à l'entier positif, noté BB(n), où n est le nombre d'états de la machine de Turing.

En septembre 2024, une équipe de plus de 20 contributeurs a annoncé avoir trouvé le cinquième numéro de castor occupé, BB(5), d'une valeur de 47 176 870. Ce résultat fait partie du projet Busy Beaver Challenge initié par Tristan Stérin, une collaboration en ligne qui vise à déterminer enfin la valeur de BB(5). L’équipe a vérifié ses résultats à l’aide d’un logiciel appelé Coq proof assistant, un outil de vérification formelle utilisé pour garantir l’exactitude des preuves mathématiques.