¡El problema del castor ocupado, un problema informático que ha durado cuarenta años, finalmente ha sido resuelto por un grupo de aficionados! Este avance no sólo conmocionó a la comunidad académica, sino que también fue reconocido por el famoso matemático Terence Tao y aclamado como el avance más importante en este campo desde 1983. Utilizando el asistente de prueba Coq, verificaron con éxito que el valor del quinto número del castor ocupado BB(5) es 47.176.870, lo que demuestra el gran potencial de la prueba asistida por software para resolver problemas matemáticos complejos y también nos proporciona información sobre el comportamiento de la máquina de Turing. y detener los problemas.
En un área misteriosa de la informática, un grupo de aficionados resolvió recientemente con éxito un problema de cuarenta años llamado el problema del castor ocupado. Este logro no sólo causó sensación en el mundo académico, sino que también fue reconocido por el famoso matemático Terence Tao, quien difundió la noticia en las redes sociales y destacó la importancia de los asistentes de prueba en la investigación matemática.
El informático Scott Aaronson también elogió este descubrimiento, considerándolo el avance más importante en la investigación de la función del castor desde 1983. Este logro marca una profunda comprensión de los límites de la teoría computacional y demuestra 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 una máquina de Turing específica que pudiera escribir la mayor cantidad de unos antes de detenerse. Una máquina de Turing es un modelo informático abstracto propuesto por Alan Turing en 1936 que realiza cálculos en una cinta magnética infinitamente larga leyendo y escribiendo 0 y 1.
Después de que en 1974 se determinara el cuarto número de castor ocupado, encontrar el quinto castor se convirtió en una cuestión abierta. Ahora, una comunidad en línea de más de 20 contribuyentes de todo el mundo, utilizando un software asistente de prueba llamado Coq, ha verificado con éxito que el quinto número BB(5) de Busy Beaver tiene un valor de 47,176,870.
Este logro no sólo entusiasmó a la comunidad, sino que también despertó el asombro del informático Damien Woods, quien comparó el progreso con la velocidad de Usain Bolt. Aunque la solución a este problema puede no ser directamente aplicable a otras áreas de la informática, para los participantes esta lucha contra la imposibilidad matemática es en sí misma la mayor recompensa.
El núcleo del problema del castor ocupado radica en comprender el comportamiento de las máquinas de Turing, específicamente su desempeño en problemas de detención. El comportamiento de una máquina de Turing está definido por un conjunto de reglas, que pueden imaginarse como una tabla. Cada regla especifica una acción que se debe realizar cuando el cabezal de lectura/escritura encuentra un 0 o un 1 en un estado específico.
Aunque las máquinas de Turing pueden quedarse atrapadas en bucles infinitos, determinar si alguna vez dejan de funcionar es un problema famoso sin resolver. El matemático Tibor Radó no quedó satisfecho con esta conclusión e inventó el "juego del castor ocupado" para explorar la naturaleza del problema de la detención agrupando las máquinas de Turing según el número de reglas que tenían.
Los primeros investigadores, como Allen Brady, exploraron este problema escribiendo programas para simular el comportamiento de las máquinas de Turing. Su trabajo y los descubrimientos de otros investigadores sentaron las bases para exploradores posteriores.
Hasta 2022, el estudiante de posgrado Tristan Stérin lanzó el Busy Beaver Challenge, un proyecto colaborativo en línea destinado a finalizar BB(5). Mediante métodos innovadores y la ayuda del asistente Coq Proof, el equipo finalmente logró encontrar el quinto castor ocupado.
Este logro no es sólo un desafío a la imposibilidad de las matemáticas, sino también una exploración de los límites de la informática. Con BB(5) confirmado, los investigadores están redactando un artículo académico que será una versión legible por humanos que complementará la prueba Coq. Al mismo tiempo, también están pensando si la exploración de BB(6) será el próximo objetivo.
Referencia: https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/
La solución al problema del castor ocupado no solo es un gran avance en el campo de las matemáticas, sino que también proporciona nuevas direcciones e ideas para futuras investigaciones de la teoría de la computación. Este logro anima a más personas a participar en la investigación de matemáticas e informática y a explorar áreas desconocidas juntas.