Una prueba controvertida en matemáticas, que ha dividido el campo durante más de una década, podría finalmente ser resuelta por un juez improbable: un programa de computadora. El centro del debate gira en torno al intento de Shinichi Mochizuki de 2012 de resolver la conjetura ABC, un problema de larga data profundamente arraigado en la naturaleza fundamental de los números.
La conjetura ABC se centra en una ecuación engañosamente simple que involucra tres números enteros: a + b = c. Plantea reglas específicas que rigen cómo se deben relacionar los números primos que componen estos números enteros. Resolver este problema aparentemente básico podría desbloquear profundos conocimientos de las matemáticas, lo que podría tener un impacto en otras conjeturas famosas como el último teorema de Fermat.
Mochizuki, profesor de la Universidad de Kyoto en Japón, presentó su prueba dentro de un marco complejo que inventó llamado teoría interuniversal de Teichmüller (IUT). Sin embargo, el puro tecnicismo y la oscuridad de la teoría IUT la hicieron en gran medida incomprensible para la mayoría de los matemáticos que intentaban verificar su trabajo. El entusiasmo inicial dio paso a la frustración cuando los expertos lucharon por descifrar sus complejidades.
Para echar más leña al fuego, en 2018, dos destacados matemáticos alemanes, Peter Scholze y Jakob Stix, identificaron un posible defecto en la demostración de Mochizuki. Mochizuki respondió a su argumento, y sin un organismo global para arbitrar las disputas matemáticas, el campo se fracturó en dos bandos: aquellos que aceptaban en gran medida la visión dominante (apoyada por la mayoría de los matemáticos) y un grupo más pequeño alineado con Mochizuki y su instituto en Kioto.
Ahora, Mochizuki propone un camino a seguir a través de la formalización: convertir su prueba de notación matemática legible por humanos a Lean, un lenguaje de programación de computadoras diseñado específicamente para una verificación matemática rigurosa. Este proceso podría potencialmente permitir que las computadoras verifiquen automáticamente la coherencia de sus argumentos, ofreciendo un nivel de objetividad sin precedentes.
Mochizuki cree que Lean está excepcionalmente equipado para sortear los complejos obstáculos lingüísticos y conceptuales que han estancado el progreso en la comprensión de la teoría IUT. Lo ve como una herramienta para liberar la verdad matemática de los posibles sesgos inherentes a la interpretación humana.
Si bien algunos expertos como Kevin Buzzard del Imperial College de Londres ven esto como una dirección prometedora, también reconocen el monumental desafío que tenemos por delante. Formalizar la teoría IUT requeriría traducir vastas extensiones de ecuaciones intrincadas a la sintaxis Lean, una tarea similar a algunos de los proyectos de formalización más grandes jamás emprendidos. Estos esfuerzos suelen implicar equipos dedicados de matemáticos y programadores que duran meses o incluso años.
Johan Commelin, de la Universidad de Utrecht (Países Bajos), aunque cautelosamente optimista, enfatiza que el éxito depende del compromiso sostenido de Mochizuki. Advierte que si el proyecto se abandona prematuramente, podría simplemente convertirse en otro capítulo de una saga prolongada marcada por disputas no resueltas.
Incluso si tiene éxito, Commelin señala que incluso con código verificado por computadora, los desacuerdos sobre la interpretación podrían persistir. Lean podría resolver contradicciones lógicas pero no necesariamente sofocar todas las diferencias filosóficas o conceptuales que rodean el trabajo de Mochizuki.
En última instancia, si bien la formalización ofrece un rayo de esperanza para resolver este duradero estancamiento matemático, queda por ver si puede superar las complejidades profundamente arraigadas y las diferentes perspectivas que han caracterizado el debate sobre la prueba de la conjetura ABC.
