En cierto sentido, la computadora y la conjetura de Collatz son una combinación perfecta. Por un lado, como señala Jeremy Avigad, lógico y profesor de filosofía en Carnegie Mellon, la noción de un algoritmo iterativo está en la base de la informática, y las secuencias de Collatz son un ejemplo de un algoritmo iterativo, procediendo paso a paso de acuerdo con a una regla determinista. De manera similar, mostrar que un proceso termina es un problema común en la informática. “Los informáticos generalmente quieren saber que sus algoritmos terminan, es decir, que siempre devuelven una respuesta”, dice Avigad. Heule y sus colaboradores están aprovechando esa tecnología para abordar la conjetura de Collatz, que en realidad es solo un problema de terminación.
“La belleza de este método automatizado es que puede encender la computadora y esperar”.
Jeffrey Lagarias
La experiencia de Heule es con una herramienta computacional llamada “solucionador de SAT”, o un solucionador de “satisfacibilidad”, un programa de computadora que determina si existe una solución para una fórmula o problema dado un conjunto de restricciones. Aunque es crucial, en el caso de un desafío matemático, un solucionador de SAT primero necesita el problema traducido, o representado, en términos que la computadora entienda. Y como dice Yolcu, estudiante de doctorado de Heule: “La representación importa, mucho”.
Una apuesta arriesgada, pero vale la pena intentarlo
Cuando Heule mencionó por primera vez abordar a Collatz con un solucionador de SAT, Aaronson pensó: “No hay forma de que esto funcione”. Pero se convenció fácilmente de que valía la pena intentarlo, ya que Heule vio formas sutiles de transformar este viejo problema que podrían hacerlo flexible. Había notado que una comunidad de científicos informáticos estaba utilizando solucionadores SAT para encontrar con éxito pruebas de terminación para una representación abstracta de la computación llamada “sistema de reescritura”. Era una posibilidad remota, pero sugirió a Aaronson que transformar la conjetura de Collatz en un sistema de reescritura podría hacer posible obtener una prueba de terminación para Collatz (Aaronson había ayudado previamente a transformar la hipótesis de Riemann en un sistema computacional, codificándolo en un pequeño Turing máquina). Esa noche, Aaronson diseñó el sistema. “Fue como una tarea, un ejercicio divertido”, dice.
“En un sentido muy literal, estaba luchando contra un Terminator, al menos un demostrador de teoremas de terminación”.
Scott Aaronson
El sistema de Aaronson capturó el problema de Collatz con 11 reglas. Si los investigadores pudieran obtener una prueba de terminación para este sistema análogo, aplicando esas 11 reglas en cualquier orden, eso probaría que la conjetura de Collatz es cierta.
Heule probó con herramientas de última generación para probar la terminación de los sistemas de reescritura, lo que no funcionó; fue decepcionante, si no tan sorprendente. “Estas herramientas están optimizadas para problemas que se pueden resolver en un minuto, mientras que cualquier enfoque para resolver Collatz probablemente requiera días, si no años, de computación”, dice Heule. Esto proporcionó motivación para perfeccionar su enfoque e implementar sus propias herramientas para transformar el problema de reescritura en un problema SAT.
HEULE MARINO
Aaronson pensó que sería mucho más fácil resolver el sistema menos una de las 11 reglas, dejando un sistema “similar a Collatz”, una prueba de fuego para el objetivo más amplio. Lanzó un desafío humano contra computadora: el primero en resolver todos los subsistemas con 10 reglas gana. Aaronson lo intentó a mano. Heule probado por el solucionador SAT: codificó el sistema como un problema de satisfacibilidad, con otra capa inteligente de representación, traduciendo el sistema a la jerga de las variables de la computadora que pueden ser 0 y 1, y luego dejó que su solucionador SAT se ejecutara en los núcleos , buscando evi dencia de terminación.
HEULE MARINO
Ambos lograron demostrar que el sistema termina con los diversos conjuntos de 10 reglas. A veces era una empresa trivial, tanto para el ser humano como para el programa. El enfoque automático de Heule tomó como máximo 24 horas. El enfoque de Aaronson requirió un esfuerzo intelectual significativo, que tomó algunas horas o incluso un día; un conjunto de 10 reglas que nunca logró probar, aunque cree firmemente que podría hacerlo con más esfuerzo. “En un sentido muy literal, estaba luchando contra un Terminator”, dice Aaronson, “al menos un demostrador del teorema de la terminación”.
Desde entonces, Yolcu ha perfeccionado el solucionador de SAT, calibrando la herramienta para que se adapte mejor a la naturaleza del problema de Collatz. Estos trucos marcaron la diferencia: aceleraron las pruebas de terminación para los subsistemas de 10 reglas y redujeron los tiempos de ejecución a meros segundos.
“La pregunta principal que queda”, dice Aaronson, “es, ¿qué pasa con el conjunto completo de 11? Intenta ejecutar el sistema en el conjunto completo y simplemente funciona para siempre, lo que tal vez no debería sorprendernos, porque ese es el problema de Collatz “.
Como lo ve Heule, la mayor parte de la investigación en razonamiento automatizado hace la vista gorda ante los problemas que requieren muchos cálculos. Pero basándose en sus avances anteriores, cree que estos problemas se pueden resolver. Otros tienen transformado Collatz tener un sistema de reescritura, pero es la estrategia de manejar un solucionador SAT ajustado a escala con un poder de cómputo formidable que podría ganar tracción hacia una prueba.
Hasta ahora, Heule ha llevado a cabo la investigación de Collatz utilizando unos 5.000 núcleos (las unidades de procesamiento alimentan las computadoras; las computadoras de consumo tienen cuatro u ocho núcleos). Como becario de Amazon, tiene una invitación abierta de Amazon Web Services para acceder a recursos “prácticamente ilimitados”, hasta un millón de núcleos. Pero es reacio a usar mucho más.
“Quiero alguna indicación de que este es un intento realista”, dice. De lo contrario, Heule siente que estaría desperdiciando recursos y confianza. “No necesito un 100% de confianza, pero realmente me gustaría tener alguna evidencia de que existe una posibilidad razonable de que tenga éxito”.
Sobrealimentar una transformación
“La belleza de este método automatizado es que se puede encender la computadora y esperar”, dice el matemático Jeffrey Lagarias, de la Universidad de Michigan. Ha jugado con Collatz durante unos cincuenta años y se ha convertido en el guardián del conocimiento, compilando bibliografías comentadas y editando un libro sobre el tema ”.El desafío definitivo.“Para Lagarias, el enfoque automatizado trajo a la mente un 2013 papel por el matemático de Princeton John Horton Conway, quien reflexionó que el problema de Collatz podría estar entre una clase elusiva de problemas que son verdaderos e “indecidibles”, pero a la vez no demostrablemente indecidibles. Como señaló Conway: “… incluso podría ser que la afirmación de que no son probables no lo sea en sí misma, y así sucesivamente”.
“Si Conway tiene razón”, dice Lagarias, “no habrá pruebas, automatizadas o no, y nunca sabremos la respuesta”.