En informática, se llama castor afanoso (busy beaver) a la máquina de Turing con n estados que escribe el máximo número de palotes (unos) antes de parar a partir de una cinta vacía; la función castor afanoso BB(n) es dicho número máximo de palotes. Propuesta por Tibor Radó en 1962 y popularizada por A. K. Dewdney en 1984, se sabe que BB(1) = 1, BB(2) = 6, BB(3) = 21, BB(4) = 107, y se había conjeturado que BB(5) ≥ 47 176 870 (Marxen y Buntrock, 1990). El proyecto internacional The Busy Beaver Challenge anunció el 2 de julio que logró demostrar que BB(5) = 47 176 870 (una demostración verificada con Coq, un demostrador automático de teoremas). En la demostración se prueba que todas las máquinas de Turing con 5 estados que ejecutan más de 47 176 870 pasos nunca paran; por tanto, ninguna es un castor afanoso. La gran dificultad no es que haya 16 679 880 978 201 máquinas de Turing con 5 estados, sino demostrar que una de ellas nunca para; la indecidibilidad del problema de la parada implica que no existe un procedimiento general para lograrlo, lo que no impide que para casos particulares se puede desarrollar.

Tristan Stérin se propuso lograr la demostración en 2020. A finales de 2021 ya había demostrado que el problema se reducía a estudiar el problema de la parada de una lista de unas 88 millones de máquinas Turing de cinco estado que ejecutaban al menos 47 176 870 pasos. Una labor para la que requería ayuda, así nació el proyecto BBChallenge en la primavera de 2022. Stérin ideó una representación gráfica (diagrama espaciotemporal) para visualizar la ejecución de cada máquina; dicha representación ayudaba a intuir las propiedades de una máquina de Turing que permiten demostrar que nunca parará (identificando bucles y patrones que se repiten ad infinitum; en la mayoría de las máquinas llega un momento en que se repiten estos bucles cada menos de mil pasos, pero para algunas de ellas, como Skelet #1 y Skelet #17, identificar las repeticiones ha requerido más de ocho mil millones de pasos).

Los participantes más relevantes del Busy Beaver Challenge, aparte de Stérin, fueron Shawn Ligocki, Justin Blanchard, Pavel Kropitz, Maja Kądziołka (clave en la formalización en Coq), Chris Xu (clave para atacar Skelet #17) y mxdys (pseudónimo). El trabajo fue intenso durante meses, pero el 10 de mayo la demostración en Coq de BB(5) ya estaba terminada (la versión final de la prueba con cuarenta mil líneas de código es de mxdys). En la actualidad, se está escribiendo el artículo científico con la demostración. La página web del proyecto Busy Beaver Challenge [web], incluye una página específica de BB(5) [web]. Si te interesa esta cuestión te recomiendo leer las piezas divulgativas de Tristan Stérin, «[July 2nd 2024] We have proved “BB(5) = 47,176,870”,»  BBChallenge, 02 Jul 2024; Ben Brubaker, «With Fifth Busy Beaver, Researchers Approach Computation’s Limits,» Quanta Magazine, 02 Jul 2024; Scott Aaronson, «BusyBeaver(5) is now known to be 47,176,870,» Shtetl-Optimized, 02 Jul 2024. En este blog también puedes leer «La función castor afanoso cumple 60 años», LCMF, 14 may 2022.

Por cierto, quizás te preguntes qué se sabe del valor de BB(6). Pavel Kropitz en 2010 descubrió que BB(6) es mayor que 10^10^10^10^10^10^10^10^10^10^10^10^10^10^10 (o sea, 10 elevado a sí mismo 15 veces). En el marco del proyecto BBChallenge se está estudiando cómo atacar este problema; pero no será fácil, pues Stérin ha descubierto una máquina de Turing con 6 estados relacionada con la conjetura de Collatz; luego para determinar BB(6) primero habrá que demostrar (o refutar) la conjetura de Collatz. Por ello, no se prevé avances significativos en los próximos años.