Dans le domaine mystérieux de l'informatique théorique, un problème vieux de quarante ans, le problème du castor affairé, a récemment été résolu par un groupe d'amateurs. Cette réussite a non seulement suscité un vif intérêt dans le monde académique, mais a également été saluée par le célèbre mathématicien Terence Tao, qui a relayé la nouvelle sur les réseaux sociaux, soulignant l'importance des assistants de preuve dans la recherche mathématique.
L'informaticien Scott Aaronson a également fait l'éloge de cette découverte, la qualifiant de progrès le plus important dans l'étude de la fonction du castor affairé depuis 1983. Cet accomplissement marque une compréhension approfondie des limites de la théorie du calcul et démontre le potentiel des preuves assistées par logiciel pour résoudre des problèmes mathématiques complexes.
Le problème du castor affairé trouve son origine il y a plus de 40 ans à Dortmund, en Allemagne, lorsque des informaticiens ont cherché à trouver la machine de Turing spécifique capable d'écrire le plus grand nombre de "1" avant de s'arrêter. Une machine de Turing est un modèle de calcul abstrait, proposé par Alan Turing en 1936, qui effectue des calculs en lisant et en écrivant des 0 et des 1 sur un ruban infiniment long.
En 1974, après la détermination du quatrième nombre du castor affairé, la recherche du cinquième est devenue un problème en suspens. Aujourd'hui, une communauté en ligne composée de plus de 20 contributeurs du monde entier, utilisant un logiciel d'assistant de preuve appelé Coq, a réussi à vérifier que la valeur du cinquième nombre du castor affairé, BB(5), est 47 176 870.
Cette réussite a non seulement enthousiasmé la communauté, mais a également suscité l'admiration de l'informaticien Damien Woods, qui a comparé cette avancée à la vitesse d'Usain Bolt. Bien que la résolution de ce problème n'ait peut-être pas d'application directe dans d'autres domaines de l'informatique, pour les participants, la lutte contre l'impossibilité mathématique est en soi la plus grande récompense.
Le cœur du problème du castor affairé réside dans la compréhension du comportement des machines de Turing, en particulier leur comportement concernant le problème de l'arrêt. Le comportement d'une machine de Turing est défini par un ensemble de règles, que l'on peut imaginer comme un tableau. Chaque règle spécifie l'opération à effectuer lorsque la tête de lecture/écriture rencontre un 0 ou un 1 dans un état donné.
Bien qu'une machine de Turing puisse tomber dans une boucle infinie, déterminer si elle s'arrêtera ou non est un problème célèbre non résolu. Le mathématicien Tibor Radó, insatisfait de cette conclusion, a inventé le « jeu du castor affairé », explorant la nature du problème de l'arrêt en regroupant les machines de Turing en fonction du nombre de règles qu'elles possèdent.
Des chercheurs précurseurs, comme Allen Brady, ont exploré ce problème en écrivant des programmes simulant le comportement des machines de Turing. Ses travaux et les découvertes d'autres chercheurs ont jeté les bases pour les explorations ultérieures.
En 2022, l'étudiant diplômé Tristan Stérin a lancé le « Busy Beaver Challenge », un projet de collaboration en ligne visant à déterminer finalement BB(5). Grâce à des méthodes innovantes et à l'aide de l'assistant de preuve Coq, l'équipe a finalement réussi à trouver le cinquième castor affairé.
Cet accomplissement représente non seulement un défi à l'impossibilité mathématique, mais aussi une exploration des limites de l'informatique. Avec la confirmation de BB(5), les chercheurs sont en train de rédiger un article scientifique, qui sera une version lisible par l'homme complétant la preuve Coq. Parallèlement, ils se demandent si l'exploration de BB(6) ne sera pas le prochain objectif.
Références : https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/