Le problème du castor occupé, problème informatique qui dure depuis quarante ans, a enfin été résolu par un groupe d'amateurs ! Ce développement révolutionnaire a non seulement choqué la communauté universitaire, mais a également été reconnu par le célèbre mathématicien Terence Tao et a été salué comme le développement le plus important dans ce domaine depuis 1983. À l’aide de l’assistant de preuve Coq, ils ont réussi à vérifier que la valeur du cinquième nombre de castor occupé BB(5) est 47 176 870, démontrant le grand potentiel de la preuve assistée par logiciel dans la résolution de problèmes mathématiques complexes, et nous fournissant également un aperçu du comportement des machines de Turing. et mettre un terme aux problèmes.
Dans un domaine mystérieux de l'informatique, un problème vieux de quarante ans appelé problème du castor occupé a récemment été résolu avec succès par un groupe d'amateurs. Cette réussite a non seulement fait sensation dans le monde académique, mais a également été reconnue par le célèbre mathématicien Terence Tao, qui a relayé la nouvelle sur les réseaux sociaux et souligné l'importance des assistants de preuve dans la recherche mathématique.
L'informaticien Scott Aaronson a également fait l'éloge de cette découverte, estimant qu'il s'agit du développement le plus important dans la recherche sur la fonction du castor depuis 1983. Cette réalisation marque une compréhension approfondie des limites de la théorie computationnelle et démontre le potentiel des preuves assistées par logiciel dans la résolution de problèmes mathématiques complexes.
Le problème du castor occupé est né il y a plus de 40 ans à Dortmund, en Allemagne, lorsque des informaticiens ont essayé de trouver une 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 informatique abstrait proposé par Alan Turing en 1936 qui effectue des calculs sur une bande magnétique infiniment longue en lisant et en écrivant des 0 et des 1.
Après la détermination du quatrième numéro de castor occupé en 1974, trouver le cinquième castor est devenu une question ouverte. Aujourd’hui, une communauté en ligne de plus de 20 contributeurs du monde entier, utilisant le logiciel d’assistance à la preuve appelé Coq, a réussi à vérifier que le cinquième nombre Busy Beaver BB(5) a une valeur de 47 176 870.
Cette réussite a non seulement enthousiasmé la communauté, mais a également suscité l'étonnement de l'informaticien Damien Woods, qui a comparé les progrès à la vitesse d'Usain Bolt. Bien que la solution à ce problème ne soit pas directement applicable à d’autres domaines de l’informatique, pour les participants, cette lutte contre l’impossibilité mathématique est en soi la plus grande récompense.
Le cœur du problème du castor occupé réside dans la compréhension du comportement des machines de Turing, en particulier de leurs performances lors des problèmes d'arrêt. Le comportement d’une machine de Turing est défini par un ensemble de règles, que l’on peut imaginer sous forme de tableau. Chaque règle spécifie une action qui doit être effectuée lorsque la tête de lecture/écriture rencontre un 0 ou un 1 dans un état spécifique.
Bien que les machines de Turing puissent rester bloquées dans des boucles infinies, déterminer si elles s’arrêtent un jour est un problème notoirement non résolu. Le mathématicien Tibor Radó n'était pas satisfait de cette conclusion et a donc inventé le « jeu du castor occupé » pour explorer la nature du problème d'arrêt en regroupant les machines de Turing en fonction du nombre de règles dont elles disposaient.
Les premiers chercheurs, comme Allen Brady, ont exploré ce problème en écrivant des programmes pour simuler le comportement des machines de Turing. Son travail et les découvertes d’autres chercheurs ont jeté les bases des explorateurs ultérieurs.
Jusqu'en 2022, l'étudiant diplômé Tristan Stérin a lancé le Busy Beaver Challenge, un projet collaboratif en ligne visant à finaliser BB(5). Grâce à des méthodes innovantes et à l'aide de l'assistant de preuve Coq, l'équipe a finalement réussi à retrouver le cinquième castor occupé.
Cette réalisation n’est pas seulement un défi à l’impossibilité des mathématiques, mais aussi une exploration des limites de l’informatique. Une fois BB(5) confirmé, les chercheurs rédigent un article académique qui sera une version lisible par l'homme qui complètera la preuve Coq. Dans le même temps, ils se demandent également si l’exploration de BB(6) deviendra la prochaine cible.
Référence : https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/
La solution au problème du castor est non seulement une avancée majeure dans le domaine des mathématiques, mais elle fournit également de nouvelles orientations et de nouvelles idées pour la recherche future en théorie informatique. Cette réalisation encourage davantage de personnes à participer à la recherche en mathématiques et en informatique et à explorer ensemble des domaines inconnus.