Una demostración de 500 páginas que nadie ha logrado leer hasta el final
Imagina que un matemático publica, de la noche a la mañana, una demostración de uno de los problemas más difíciles de su campo y que, doce años después, nadie es aún capaz de decir si es correcta o falsa. Eso es exactamente lo que ocurre desde 2012 con la conjetura abc, y quizá sea el mayor escándalo silencioso de la historia de las matemáticas modernas. Para acabar con ello, unos investigadores han decidido dejar el veredicto en manos de una máquina.
La conjetura abc: un problema de apariencia sencilla y profundidad abismal
Antes de entrar en materia, sentemos las bases. La conjetura abc es un enunciado sobre números enteros, formulado en los años 1980 por los matemáticos Joseph Oesterlé y David Masser. Su idea central puede resumirse así: si tres enteros a, b y c verifican la ecuación a + b = c, los factores primos que componen esos tres números no pueden ser todos muy pequeños a la vez. Dicho de otro modo, una suma sencilla entre dos enteros condiciona la estructura profunda de sus divisores.
Esta conjetura puede parecer inofensiva formulada así, pero sus implicaciones son considerables: si se demostrara, implicaría automáticamente la demostración de decenas de otros teoremas importantes de teoría de números, la rama de las matemáticas que estudia las propiedades de los enteros. El último teorema de Fermat, por ejemplo, se derivaría de ella casi como un corolario. La conjetura abc es, por tanto, una especie de clave de bóveda: validarla abre de golpe decenas de puertas.
Mochizuki, el solitario de Kioto
En agosto de 2012, Shinichi Mochizuki, profesor de la Universidad de Kioto, publica en su sitio web personal cuatro artículos que suman más de 500 páginas. En ellos anuncia haber demostrado la conjetura abc. Pero la demostración no se parece a nada conocido: se apoya en una teoría completamente nueva, que Mochizuki desarrolló en solitario durante una década y que denomina la teoría de los espacios de Teichmüller interuniversales, o IUT para los amigos.
¿El problema? Esta teoría inventa sus propios objetos matemáticos, sus propias notaciones, sus propias reglas del juego. Para comprender la demostración, primero hay que aprender un lenguaje que nadie más ha hablado jamás. Algunos de los matemáticos más brillantes del mundo lo han intentado. Muchos abandonaron tras semanas o meses de esfuerzo. Peter Scholze y Jakob Stix, dos gigantes de la teoría de números, acabaron afirmando en 2018 que habían identificado un fallo concreto en la argumentación: un paso clave del razonamiento que, según ellos, no se sostiene.
«No entendemos por qué se supone que este paso debe funcionar y no creemos que funcione.» — Peter Scholze y Jakob Stix, 2018
—
Mochizuki, por su parte, ha sostenido que sus críticos sencillamente no habían comprendido su teoría. Respondió extensamente, punto por punto, sin conceder jamás el menor error. Y ahí se detuvo el diálogo. Se formaron dos bandos: quienes creen que la demostración es correcta —principalmente colaboradores cercanos de Mochizuki en Japón— y quienes consideran que está llena de agujeros. El resto de la comunidad, la inmensa mayoría, sencillamente ha renunciado a pronunciarse.
Por qué una demostración puede seguir sin resolverse durante diez años
Este caso ilustra un límite profundo del sistema de validación de las matemáticas. En principio, una demostración matemática es correcta o incorrecta: no hay zonas grises. Pero, en la práctica, la validación se basa en la peer review, es decir, la revisión por pares: otros especialistas del campo que comprueban cada paso del razonamiento. Este sistema funciona muy bien cuando una demostración se inscribe en un lenguaje compartido. Se derrumba cuando la demostración reinventa ese lenguaje desde cero.
Nadie cobra por dedicar seis meses a aprender una teoría entera solo para comprobar si es coherente. Los matemáticos tienen clases que impartir, artículos que publicar y carreras que construir. Auditar la demostración de Mochizuki supone una inversión colosal con un retorno incierto. Resultado: la demostración sí se publicó en una revista —las Publications of the Research Institute for Mathematical Sciences de Kioto, de la que el propio Mochizuki es editor jefe, lo que suscitó críticas por conflicto de intereses—, pero sin obtener jamás la validación informal de la comunidad internacional.
El ordenador como árbitro de última instancia
En este contexto de bloqueo total surge un nuevo enfoque: la verificación formal asistida por ordenador. El principio es el siguiente. Programas especializados —denominados proof assistants, o asistentes de demostración— permiten traducir una demostración matemática a un lenguaje formal que la máquina puede comprobar paso a paso, mecánicamente, sin cansancio ni sesgos. Si un paso no se sostiene, el ordenador lo detecta.
Unos investigadores han comenzado a formalizar partes fundamentales de la teoría IUT en uno de estos asistentes de demostración. El objetivo es preciso: comprobar el paso exacto que Scholze y Stix cuestionaron. Si el ordenador confirma el fallo, el debate queda zanjado. Si, por el contrario, valida el paso, obligará a la comunidad a reconsiderar sus objeciones.
No es una tarea trivial. Formalizar matemáticas avanzadas en un asistente de demostración exige un trabajo considerable, a veces años para unas pocas páginas. Pero quizá sea la única forma de salir de un callejón sin salida que los humanos por sí solos no han logrado resolver.
Las lecciones de un escándalo matemático
Más allá del caso Mochizuki, este asunto plantea preguntas que trascienden con mucho a un solo hombre o una sola conjetura. ¿Cómo debe tratar la comunidad matemática las teorías radicalmente nuevas, aquellas que exigen años de aprendizaje antes siquiera de poder evaluarlas? ¿Quién debe asumir el coste de la verificación? Y, si nadie lo hace, ¿puede considerarse realmente una demostración que nadie ha leído?
El auge de los asistentes de demostración abre una vía seria. Las matemáticas formalizadas pueden ser verificadas por cualquiera que disponga del programa adecuado. Ya no dependen de la buena voluntad de un puñado de especialistas sobrecargados. Algunos investigadores ya defienden que las grandes demostraciones vayan acompañadas sistemáticamente de su versión formal. Sería una revolución en la manera de hacer y transmitir las matemáticas.
Mientras tanto, el veredicto de la máquina se espera con una impaciencia teñida de inquietud. Pues, si el ordenador confirma el fallo, habrá que extraer una conclusión incómoda: durante más de una década, la comunidad matemática mundial ha sido incapaz de validar o invalidar uno de sus propios resultados supuestamente fundamentales. Y eso es un fallo del sistema, no solo de una demostración.
Conceptos clave
Para los amantes de las matemáticas
La conjetura abc se formula con precisión mediante la noción de radical de un entero. Para un entero n, se define rad(n) como el producto de todos los factores primos distintos de n, sin tener en cuenta sus multiplicidades. Por ejemplo, rad(12) = rad(2² × 3) = 2 × 3 = 6. La conjetura estipula entonces que, para todo número real ε > 0, solo existe un número finito de ternas de enteros (a, b, c) coprimos dos a dos, que verifican a + b = c y tales que c > rad(abc)1+ε. Dicho de otro modo, los casos en que c es «mucho mayor» que el radical del producto abc son extremadamente raros. Esta formulación recoge la idea de que la aparición de potencias elevadas en la descomposición en factores primos de una suma es una anomalía, no la norma.
