Las computadoras pueden verificar pruebas matemáticas.
monsitj/Getty Images
Uno de los debates más controvertidos en matemáticas podría resolverse con la ayuda de una computadora, lo que podría poner fin a una amarga discusión sobre una demostración compleja que se ha prolongado durante más de una década.
El problema comenzó en 2012, cuando Shinichi Mochizuki, de la Universidad de Kyoto (Japón), sorprendió al mundo matemático con una extensa prueba de 500 páginas de la conjetura ABC, un importante problema sin resolver que ataca el corazón mismo de lo que son los números. La prueba utilizó un marco altamente técnico y abstruso inventado por Mochizuki, llamado teoría interuniversal de Teichmüller (IUT), que parecía impenetrable incluso para la mayoría de los matemáticos expertos que intentaban comprenderla.
La conjetura ABC, que ya tiene más de 40 años, involucra una ecuación aparentemente simple de tres números enteros, a + b = c, y dicta cómo los números primos que componen estos números deben relacionarse entre sí. Además de brindar información profunda sobre la naturaleza fundamental de cómo interactúan la suma y la multiplicación, la conjetura tiene implicaciones para otras conjeturas matemáticas famosas, como el último teorema de Fermat.
Estas posibles ramificaciones hicieron que los matemáticos inicialmente se entusiasmaran con la verificación de la prueba, pero los primeros esfuerzos fracasaron y Mochizuki se lamentó de que no se hubieran hecho más esfuerzos para digerir el trabajo. Luego, en 2018, dos destacados matemáticos alemanes, Peter Scholze de la Universidad de Bonn y Jakob Stix de la Universidad Goethe de Frankfurt, anunciaron que habían localizado una posible grieta en la armadura de la prueba.
Pero Mochizuki rechazó su argumento y, sin un gran órgano de decisión que dictaminara quién tenía razón o quién no, la validez de la teoría IUT se congeló en dos bandos: por un lado, la mayor parte de la comunidad matemática; por el otro, un pequeño grupo de investigadores vagamente afiliados a Mochizuki y al Instituto de Investigación de Ciencias Matemáticas de Kioto, donde es profesor.
Ahora, Mochizuki ha propuesto una posible solución al estancamiento. Ha sugerido traducir la prueba de su forma actual, en una notación matemática diseñada para humanos, a un lenguaje de programación llamado Lean, que podría ser revisado y verificado automáticamente por una computadora.
Este proceso, llamado formalización, es un área de investigación en curso que podría cambiar completamente la forma en que se hacen matemáticas. Se ha sugerido antes formalizar la prueba de Mochizuki, pero esta es la primera vez que ha indicado su deseo de seguir adelante con el proyecto.
Mochizuki no respondió a una solicitud de comentarios para este artículo, pero en un informe reciente, argumentó que Lean sería muy adecuado para desenredar los tipos de desacuerdos entre matemáticos que han impedido la aceptación generalizada de su prueba: “[Lean] es la mejor y quizás la única tecnología… para lograr un progreso significativo con respecto al objetivo fundamental de liberar la verdad matemática del yugo de la dinámica social y política”, escribe Mochizuki.
Según Mochizuki, estaba convencido de los méritos de la formalización después de asistir a una reciente conferencia sobre Lean en Tokio en julio, en particular después de ver su capacidad para manejar el tipo de estructuras matemáticas que, según él, son esenciales para su teoría IUT.
Esta es una dirección potencialmente prometedora para ayudar a salir del estancamiento, dice Kevin Buzzard del Imperial College de Londres. “Si está escrito en Lean, entonces no es una locura, ¿verdad? Muchas cosas en los periódicos están escritas en un lenguaje muy extraño, pero si puedes escribirlo en Lean, entonces significa que al menos este lenguaje extraño se ha convertido en algo completamente bien definido”, dice.
“Queremos entender el porqué [of IUT]y lo hemos estado esperando durante más de 10 años”, dice Johan Commelin de la Universidad de Utrecht en los Países Bajos. “Lean podría ayudarnos a comprender esas respuestas”.
Sin embargo, tanto Buzzard como Commelin dicen que formalizar la teoría IUT sería una tarea gigantesca e implicaría traducir resmas de ecuaciones matemáticas que actualmente sólo existen en forma legible por humanos. Este proyecto estaría a la par de algunos de los esfuerzos de formalización más grandes que jamás se hayan completado, que a menudo involucran equipos de matemáticos expertos y programadores Lean, y que demoran meses o años.
Esta desalentadora perspectiva puede ser una propuesta poco atractiva para el pequeño puñado de matemáticos calificados para asumir el proyecto. “La gente va a tener que tomar una decisión importante sobre si quiere dedicar gran parte de su tiempo a trabajar en un proyecto que, en última instancia, podría resultar un fracaso”, dice Buzzard.
Pero incluso si los matemáticos logran completar el proyecto y el código Lean muestra que el teorema de Mochizuki no tiene contradicciones, los matemáticos, incluido el propio Mochizuki, aún podrían pelear por su significado, dice Commelin.
“Lean puede tener un gran impacto y poner fin a la controversia, pero sólo si Mochizuki realmente se apega a su nueva resolución de formalizar su trabajo”, afirma. “Si se aleja después de cuatro meses y dice: ‘Está bien, intenté esto, pero Lean es demasiado estúpido para entender mi prueba’, entonces es solo un nuevo capítulo en una serie muy larga de capítulos en los que todavía estamos atrapados con un problema social”.
Y, a pesar de todo el optimismo que Mochizuki muestra hacia Lean, también está de acuerdo con sus críticos en que interpretar el significado del código podría llevar a mayores desacuerdos, escribiendo que Lean “no parece constituir en este momento ningún tipo de” cura mágica “para la resolución completa de los problemas sociales y políticos”.
Sin embargo, Buzzard tiene la esperanza de que una formalización exitosa pueda, al menos, hacer avanzar la saga de una década, especialmente si Mochizuki tiene éxito. “No se puede discutir con el software”, afirma.
Temas: