En 2012, Shinichi Mochizuki publicó un artículo que afirmaba proporcionar una prueba de la conjetura ABC en teoría de números.
Noticias / Alamy
Una de las demostraciones más acérrimas de las matemáticas modernas puede estar a punto de ser desenredada. Dos proyectos, ambos destinados a utilizar un programa informático para arrojar nueva luz sobre la controversia, ya están en marcha y uno de ellos ya lleva más de dos años funcionando en secreto. Los avances son una señal positiva de que la disputa podría encontrar una solución, dicen los matemáticos.
La saga comenzó en 2012 cuando Shinichi Mochizuki de la Universidad de Kyoto, Japón, afirmó haber demostrado una idea famosa llamada conjetura ABC, y publicó en línea una prueba de 500 páginas. La conjetura es sencilla de formular y se refiere a los números primos involucrados en las soluciones de la ecuación a + b = c y cómo estos números se relacionan entre sí. Pero resolverlo requiere conocimientos profundos sobre la naturaleza de cómo interactúan la suma y la multiplicación. La respuesta también tiene implicaciones de largo alcance para otras disciplinas matemáticas.
La prueba de Mochizuki fue una bomba matemática, pero a muchos de sus colegas les resultó difícil entenderla porque incluía nuevas técnicas y conceptos, que él denominó colectivamente teoría interuniversal de Teichmüller (IUT). Destacados matemáticos pasaron los meses siguientes intentando aclarar el trabajo de Mochizuki, incluso en conversaciones con el propio Mochizuki, pero la exactitud de la prueba llegó a un punto muerto.
En 2018, después de que dos destacados matemáticos (Peter Scholze de la Universidad de Bonn y Jakob Stix de la Universidad Goethe de Frankfurt, ambos en Alemania) anunciaran que habían identificado un posible error, no hubo más avances. Mochizuki y un grupo de colegas cercanos, principalmente en la Universidad de Kyoto, sostuvieron que la prueba era correcta, mientras que una gran parte de la comunidad matemática argumentó que la prueba era, en el mejor de los casos, indescifrable y, en el peor, fatalmente defectuosa.
El año pasado, sin embargo, Mochizuki ofreció una rama de olivo a sus detractores y un posible camino a seguir. Ha habido un inmenso progreso en un área de las matemáticas llamada formalización, donde las pruebas matemáticas escritas se traducen a un lenguaje informático que puede verificar su exactitud automáticamente. Un lenguaje en particular, llamado Lean, fue el que más atrajo a Mochizuki. Escribió en ese momento que: “[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”.
Ahora, los esfuerzos para formalizar la prueba de Mochizuki de la conjetura ABC en Lean están oficialmente en marcha, con al menos dos grupos matemáticos separados anunciando avances, incluido uno dirigido por Mochizuki y otro que ha estado operando en secreto durante más de dos años, pero que se ha topado con un obstáculo.
A finales de 2023, Kato Fumiharu, del Centro de Matemáticas ZEN de Japón, inició el proyecto de geometría Lean y Anabeliana (LANA), reclutando a matemáticos que estaban familiarizados con el trabajo de Mochizuki, así como a expertos en Lean que habían formalizado otros grandes proyectos matemáticos. El objetivo principal era “simplemente resolver la controversia de una vez por todas”, dice Adam Topaz de la Universidad de Alberta, Canadá, a quien Fumiharu reclutó para ayudar a formalizar la prueba.
En una conferencia de prensa el mes pasado anunciando el proyecto, Fumiharu dijo que los miembros habían llegado a una “comprensión profunda” de la idea de Mochizuki en los últimos años, pero también había un punto específico en el que no podían avanzar, que está estrechamente relacionado con el área que Scholze y Stix identificaron como que contenía un posible error en 2018. “Básicamente, nos hemos quedado estancados al tratar de entender un punto particular en IUT”, dice Topaz. “Aislamos este punto hace casi un año y medio, y originalmente pensamos que sólo necesitábamos comprender más la teoría para poder superar este problema potencial”.
Pero incluso después de intentar entenderlo a través de varios talleres y comunicación indirecta con Mochizuki a través de un intermediario, Fumiharu y sus colegas no pudieron avanzar.
En un desarrollo separado, Mochizuki y sus colegas también iniciaron un proyecto para formalizar la prueba utilizando Lean. Pero están menos interesados en demostrar que es correcto, ya que Mochizuki sostiene que ya es correcto. En cambio, ve el valor del proyecto más en la comunicación.
“Este aspecto de verificación no es un punto central de interés”, dijo Mochizuki en una conferencia reciente en la Universidad de Exeter, Reino Unido. “La importancia de la formalización Lean radica en producir un registro preciso de la estructura lógica de IUT que sea inmune a falsas interpretaciones erróneas y, por lo tanto, pueda usarse para comunicar esta simplicidad de una manera máximamente eficiente o precisa a otros matemáticos”.
El enfoque de Mochizuki y su equipo es centrarse en el área controvertida de la prueba en la que el proyecto LANA quedó estancado y que Scholze y Stix identificaron por primera vez, antes de pasar a formalizar un plan con cuatro etapas más. Mochizuki afirma que han comenzado a hacer esto produciendo 70 líneas de código Lean como comienzo, aunque aún no está disponible públicamente.
Esto no es mucho código, dice Kevin Buzzard del Imperial College de Londres. “Serán mucho más que 70 líneas. En 70 líneas, estás luchando por demostrar un par de teoremas de nivel universitario, y mucho menos una prueba gigantesca”.
Sin embargo, sigue siendo uno de los avances más prometedores y significativos en la comprensión de la prueba de Mochizuki desde que se anunció por primera vez. “No ha habido ningún movimiento, no ha habido información nueva interesante de relevancia alguna, y esta es la primera vez que uno siente que tal vez las cosas realmente se están moviendo”, dice Buzzard.
Topaz está de acuerdo en que, a pesar de las dificultades, todavía parece haber un posible camino a seguir, especialmente porque Mochizuki se comunicaba abiertamente con el proyecto LANA, a pesar de que los esfuerzos de los grupos seguían siendo distintos.
“Ahora que existe este diálogo con Mochizuki usando Lean, soy bastante optimista de que podría haber una solución a esta controversia”, dice Topaz. “Si algo me da mayor optimismo en este momento es que tenemos este diálogo de ida y vuelta con el grupo de Mochizuki”.
Temas: