En un enigmático campo de la informática, un problema de cuarenta años de antigüedad, el problema del castor ocupado, ha sido resuelto recientemente por un grupo de aficionados. Este logro no solo ha causado sensación en el mundo académico, sino que también ha recibido el reconocimiento del famoso matemático Terence Tao, quien compartió la noticia en las redes sociales y destacó la importancia de los asistentes de prueba en la investigación matemática.
El científico informático Scott Aaronson también elogió este descubrimiento, considerándolo el avance más significativo en el estudio de la función del castor ocupado desde 1983. Este logro marca una comprensión profunda de los límites de la teoría de la computación y muestra el potencial de las pruebas asistidas por software para resolver problemas matemáticos complejos.
El problema del castor ocupado se originó hace más de 40 años en Dortmund, Alemania, cuando los científicos informáticos intentaron encontrar la máquina de Turing específica que pudiera escribir la mayor cantidad de "1" antes de detenerse. Una máquina de Turing es un modelo computacional abstracto, propuesto por Alan Turing en 1936, que realiza cálculos leyendo y escribiendo 0 y 1 en una cinta infinitamente larga.
Después de que se determinara el cuarto número de castor ocupado en 1974, la búsqueda del quinto se convirtió en un problema abierto. Ahora, una comunidad en línea de más de 20 colaboradores de todo el mundo, utilizando el software asistente de prueba llamado Coq, ha verificado con éxito el valor del quinto número de castor ocupado BB(5) como 47,176,870.
Este logro no solo ha entusiasmado a la comunidad, sino que también ha sorprendido al científico informático Damien Woods, quien comparó este avance con la velocidad de Bolt. Aunque la solución a este problema puede no tener una aplicación directa en otras áreas de la informática, para los participantes, la lucha contra la imposibilidad matemática en sí misma es la mayor recompensa.
El núcleo del problema del castor ocupado radica en comprender el comportamiento de las máquinas de Turing, especialmente su comportamiento en el problema de la detención. El comportamiento de una máquina de Turing está definido por un conjunto de reglas, que se pueden imaginar como una tabla. Cada regla especifica la operación que debe realizar la cabeza de lectura/escritura cuando encuentra un 0 o un 1 en un estado particular.
Aunque una máquina de Turing puede entrar en un bucle infinito, determinar si se detendrá o no es un famoso problema sin resolver. El matemático Tibor Radó no estaba satisfecho con esta conclusión y, por lo tanto, inventó el "juego del castor ocupado", explorando la naturaleza del problema de la detención al agrupar las máquinas de Turing según la cantidad de reglas que poseen.
Investigadores anteriores, como Allen Brady, exploraron este problema mediante la programación para simular el comportamiento de las máquinas de Turing. Su trabajo y los descubrimientos de otros investigadores sentaron las bases para exploraciones posteriores.
Hasta 2022, el estudiante de posgrado Tristan Stérin lanzó el "Desafío del Castor Ocupado", un proyecto de colaboración en línea destinado a determinar finalmente BB(5). Gracias a métodos innovadores y la ayuda del asistente de prueba Coq, este equipo finalmente logró encontrar el quinto castor ocupado.
Este logro no solo representa un desafío a la imposibilidad matemática, sino también una exploración de los límites de la informática. Con la confirmación de BB(5), los investigadores están redactando un artículo académico, que será una versión legible para humanos que complementa la prueba de Coq. Al mismo tiempo, se preguntan si la exploración de BB(6) será el próximo objetivo.
Referencias: https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/