¡Qué fácil es admirar una obra de arte!, pero ¡qué difícil generarla! La creación artística es semejante a la creación matemática. Todos podemos apreciar la prueba de Euclides de la infinitud de los primos, pero la mayoría se siente incapaz de generar una demostración matemática. Unos admirarán la música clásica, otros el rock, unos prefieren la pintura de Velázquez, otros a Kandinsky, unos el teatro, otros el cine. No habrá nadie que no reconozca que alguna manifestación artística les conmueve. Pero qué difícil es ser un artista. Para quitarnos la responsabilidad de no ser creativos invocamos la genialidad.
Difícil de encontrar pero fácil de admirar.
Hoy comentamos no una publicación matemática sino un hito en la práctica de la matemática. El día 5 de este mes de junio, por primera vez en la historia, un matemático, Peter Scholze, ha comprobado su demostración de un teorema difícil mediante un ordenador, más adelante explicaremos su conexión con mis comentarios anteriores sobre la creación artística y matemática.
Dudas en Matemáticas
Las matemáticas pasan por ser un terreno claro y nítido. Dos y dos son cuatro, sin discusión. Pero esto, que es cierto en general, no deja de tener sus matices. Situaciones de confusión se han dado con frecuencia. Abel, el matemático noruego, tuvo que poner orden en el estudio de las series infinitas, en este caso la falta de definiciones precisas había producido una confusión. La escuela italiana de geometría algebraica que floreció entre 1835 y 1935, con nombres prestigiosos como Enriques, Severi y Castelnuovo, terminó aceptando principios no rigurosos que llevaron a obtener resultados contradictorios. La geometría algebraica moderna, liderada por Grothendieck, acabó con esta situación consiguiendo un tratamiento completamente riguroso del tema.
El esfuerzo de axiomatización de la matemática en el siglo XX parecía haber acabado completamente con estos problemas que en muchas ocasiones se debieron a definiciones imprecisas. Pero ha surgido otro problema importante, la complejidad. Hay muchos ejemplos, pero escogeré uno para explicar la situación actual. El teorema de la clasificación de los grupos simples finitos. Estos grupos son como los componentes de cualquier grupo finito. La demostración del teorema que los describe a todos uno a uno consiste en decenas de miles de páginas, distribuidas en cientos de revistas, escritas por cientos de matemáticos y publicadas entre 1995 y 2004. Gorenstein y otros están tratando de escribir una prueba unificada, llevan publicados 9 volúmenes y esperan necesitar por lo menos otros cinco. Con demostraciones tan complicadas no es sorprendente que surjan dudas sobre su validez.
Hay casos extremos como el del problema de Busemann-Petty y su (doble) solución por Gaoyong Zhang. Este matemático ha publicado dos artículos en la mejor revista matemática:
[1] Zhang, Gaoyong, Intersection bodies and the Busemann-Petty inequalities in \(\textbf{R}^4\), Ann. of Math. 140 (1994) 331–346.
[2] Zhang, Gaoyong, A positive solution to the Busemann-Petty problem in \(\textbf{R}^4\), Ann. of Math. 149 (1999) 535–543.
En [1] Zhang demuestra que la solución al problema de Busemann-Petty es negativa en \(\textbf{R}^4\). En [2] demuestra que pasa justo lo contrario. Un caso en que el revisor dio por bueno un razonamiento incorrecto. Pero el que entienda la dificultad de leer matemáticas no se sorprenderá demasiado de que estas cosas sucedan.
El matemático Kevin Buzzard trabajaba hasta el año 2017 en geometría algebraica. Casos como el anterior de las pruebas de Zhang le llevan a tratar de encontrar un remedio a esta situación. De hecho comprobar una demostración, verificarla, es una tarea mecánica para la que existen algoritmos, mientras que para la creación de las demostraciones no se conoce ninguno.
Buzzard encontró que ya existían programas para verificar la implementación de los algoritmos en los ordenadores (cuando volamos en un avión estamos confiando nuestra integridad física en programas que deben ser fiables). Estos programas sirven también para el chequeo de las pruebas matemáticas. Buzzard eligió uno de esos programas ya existentes: Lean.
Para que un ordenador pueda verificar una demostración, es necesario enseñar al ordenador la matemática que se usa en la prueba. Es decir, el ordenador debe conocer las definiciones anteriores y los teoremas principales. Por este motivo, la primera tarea es «enseñar» la matemática de una licenciatura al ordenador. En esa tarea se va confirmando que las demostraciones de todos estos teoremas son correctas. Este es el objetivo del proyecto Xena liderado por Buzzard.
El reto: Liquid Tensor Experiment
Pocos en el público en general tendrán noticia de Peter Scholze.
A los 16 años supo de la prueba de Wiles del último teorema de Fermat y se propuso entenderla. Esto le motivó a seguir un camino especial para estudiar lo que necesitaba con ese propósito. Hoy día a sus 33 años es una estrella entre los matemáticos. Uno de sus primeros éxitos (con 22 años) fue simplificar una demostración que ocupaba un libro de 288 páginas escrito por Michael Harris y Richard Taylor, reduciéndola a un trabajo de 37 páginas. Hoy día es medalla Fields por su creación de los espacios perfectoides, que son un instrumento que ha dado ya numerosos frutos en geometría algebraica.
El 5 de diciembre de 2020 publicó un reto en la página web del proyecto Xena promovido por Buzzard para enseñar matemáticas a Lean:
Probar el teorema siguiente:
Teorema. (Clausen, Scholze) Sean \(0<p'<p\le 1\) dos números reales y \(S\) un conjunto profinito y sea \(V\) un espacio \(p\)-Banach. Sea \(\mathcal M_{p’}(S)\) el espacio de las \(p’\)-medidas sobre \(S\). Entonces $$\text{Ext}^i_{\text{Cond}(\text{Ab})}(\mathcal M_{p’}(S), V)=0$$ para todo \(i\ge 1\).
Scholze explica en su entrada en el blog de Buzzard la importancia del teorema en su intento de convertir el análisis funcional clásico en una rama del álgebra. También que la prueba de este teorema es extraordinariamente complicada, de manera que aún tiene ciertas dudas. Más precisamente, Scholze está «99.9% seguro» de que su prueba es correcta. Pero el resultado es básico para el trabajo posterior; se usará en el futuro como una caja negra. Los que lo usen no tendrán la motivación real de comprobarlo. Y piensa por esto que es especialmente importante estar completamente seguro de su validez.
La respuesta al reto
El reto de Scholze fue asumido por un grupo de matemáticos liderados por Johan Commelin, que en un tiempo record han conseguido formalizar gran parte de la prueba.
Hace unos días, el 5 de junio, Scholze ha vuelto a escribir en el blog de Buzzard:
Aunque el reto no se ha completado aún, estoy emocionado de anunciar que el experimento ha verificado la totalidad de la parte de la demostración de la que no estaba seguro. Me parece absolutamente una locura que los programas de verificación de demostraciones sean capaces en un tiempo muy razonable de verificar formalmente investigación original muy complicada.
Scholze pasa a explicar con más detalle el proceso. Para verificar la prueba hay que desmenuzarla en pequeños pasos. Eso hace que se alcance un grado de comprensión mayor. Scholze explica: Cuando intentaba demostrar el resultado, parte de la dificultad es que era incapaz de retener todos los detalles en mi RAM. Se refiere a tener presentes todos los detalles simultáneamente. El experimento hizo la prueba considerablemente más explícita y más elemental.
El sueño de Leibniz hecho realidad
Leibniz fue un maestro de la notación. A él debemos la notación $$\int f(x)\,dx$$ para representar el área definida por una función (lo que, al añadir los límites de integración, hoy llamamos integral de Riemann). Pero Leibniz soñaba con un lenguaje simbólico como el matemático, de forma que, expresada en ese lenguaje, cualquier controversia quedara reducida a un mero cálculo como en matemáticas. Más adelante los lógicos han demostrado que efectivamente la comprobación de una demostración formal es un mero cálculo, para el que puede diseñarse un algoritmo. Podemos decir que el experimento de Scholze-Buzzard es el primer ejemplo en que una controversia se decide mediante un cálculo. La prueba ha sido verificada mecánicamente. El experimento es la realización del sueño de Leibniz. Solo que Leibniz ya daba por hecho que en matemáticas no había controversia y él pensaba en cualquier tema de la vida, la política o la moral.
Pero ya vimos que sí que hay controversia en matemáticas. Es que los matemáticos no escriben demostraciones formales. No tenemos necesidad de hacer explícitos muchos pasos. Eso es necesario, de otro modo las demostraciones tendrían muchos pasos en cierto modo irrelevantes y que harían la comprobación imposible por tediosa para una persona (humana).
Uno piensa en la posibilidad de que dentro de unos años el proceso de referato se automatice. Que un artículo no sea aceptado hasta que sus demostraciones queden verificadas por Lean o cualquier otro verificador de pruebas que se estime conveniente. No creo que eso esté muy lejos. Prácticamente ya tenemos los medios.
Ahora nos adentraremos en un terreno mucho más especulativo, pero del que no puedo dejar de pensar.
Feynman y la inteligencia artificial
Feynman (1918-1988) fue premio Nobel de física y es una personalidad realmente interesante. (El que no lo conozca no debería dejar de leer algún capítulo de su curso de física, probablemente querrá leer alguno más, y también puede ver el libro ¿Está usted de broma, Sr. Feynman?.) En el año 1985, en una conferencia, Feynman responde a la pregunta de un espectador: ¿Cree que habrá alguna vez una máquina más inteligente que una persona? En la respuesta, Feynman pone el ejemplo de interpretar las imágenes. Cosas que una persona hace instantáneamente son muy difíciles. Él no afirma que nunca llegarán, pero que no sabemos cómo hacer que una máquina reconozca patrones, formas o configuraciones. Han pasado pocos años desde entonces. Feynman se sorprendería hoy al ver que los ordenadores ya sustituyen a los humanos en la conducción de vehículos; ¿llegarán a sustituir a los humanos en la creación matemática? ¿Y en la creación artística? Son preguntas inquietantes. Pero entre la digitalización de la primera imagen hasta la capacidad de interpretarlas en tiempo real para dejar en sus manos la conducción de un vehículo no han pasado más de 30 o 40 años.
El experimento Scholze-Buzzard es como el inicio de la digitalización de las pruebas. No sabemos si una vez que el programa Lean aprenda toda la matemática que estudia un doctorando no será posible que se inicie un proceso diferente.
Creación matemática
Hemos visto que la comprobación de una demostración es una tarea mecánica, pero no su creación. Lean necesita la prueba para verificarla. Pero, por ejemplo Scholze, ¿cómo demuestra el teorema? Aquí estamos ante un ejemplo del problema \(P\ne NP\). Dado un enunciado matemático \(T\), preguntamos ¿es \(T\) un teorema?, ¿existe una prueba de \(T\) de longitud \(<C\)? Si nos dan la prueba, un programa mecánico nos dará la respuesta a esta pregunta (verificando la prueba), en un tiempo proporcional a \(C\).
Pero si nos dan solo el enunciado \(T\), el único algoritmo que conocemos para obtener la prueba es escribir todas las posibles combinaciones de símbolos de longitud \(<C\) y comprobar si cada una de esas combinaciones es o no una prueba. Ese algoritmo tardaría un tiempo demasiado largo.
Decimos que \(P= NP\) si siempre que tenemos un algoritmo para validar la solución a nuestro problema en tiempo razonable, podemos también generar la solución en tiempo razonable. En nuestro caso sería decir que podemos generar la prueba en tiempo razonable. Todo el mundo piensa que eso no es así, que \(P\ne NP\). Que para generar la prueba es necesario un genio, como Scholze.
El algoritmo que nadie quiere ver
La práctica matemática nos dice que los problemas se resuelven, que no es tan difícil. Preguntas que en su momento parecieron imposibles, como la cuadratura del círculo, el último teorema de Fermat, la hipótesis del continuo, la conjetura de Poincaré y un largo etcétera, están resueltas, o con una solución o habiendo demostrado la imposibilidad de esta con los axiomas actuales. La demostración ha tardado en obtenerse, pero no podemos decir que esta solución haya tardado mucho en relación a la longitud de la prueba, que es lo importante aquí.
Y, sobre todo, tenemos un algoritmo, un algoritmo que nadie parece ver. En primer lugar, tenemos el cerebro. ¿Cómo actúa un matemático creativo? Estudia los conceptos relacionados, las demostraciones de las propiedades fundamentales de estos conceptos. Esto da vida en su cerebro a imágenes que bullen dentro de su mente, chocan y se entrecruzan. Este estado de ebullición es generado muchas veces por el deseo de resolver un problema concreto, las imágenes se van haciendo cada vez más claras. Cobran vida, nacen y mueren. Hay muchas descripciones de esta situación, y la vivencia de cada matemático no es siempre la misma. Podemos destacar la de Poincaré en su libro Ciencia y Método en el capítulo dedicado a la creación matemática. Wiles también nos ha dado una descripción:
Quizás puedo describir mejor mi experiencia de hacer matemáticas comparándola con una travesía por una mansión oscura e inexplorada. Entras en la primera habitación y está completamente a oscuras. Vas tropezando con los muebles, pero generalmente terminas por aprender dónde está situado cada mueble. Finalmente, en seis meses más o menos, encuentras la llave de la luz, la enciendes, y repentinamente todo se ilumina. Ves exactamente dónde estabas. Entonces entras en la siguiente habitación y pasas otros seis meses en la oscuridad. Por tanto, cada una de estas iluminaciones, que a veces son momentáneas, y en otras ocasiones duran un día o dos, son la culminación de —y no pueden existir sin— los muchos meses de tropezones en la oscuridad que le preceden.
El algoritmo para resolver los problemas matemáticos y encontrar las pruebas de los teoremas conjeturados es el siguiente: toma jóvenes motivados por la matemática. Muéstrales las conjeturas, proponles problemas relacionados que estén a su alcance. Proponles que estudien los trabajos relacionados y las herramientas próximas. Déjalos soñar y en unos años habrán encontrado las pruebas o construido edificios y herramientas con los que la siguiente generación estarán mejor equipados.
El método es completamente seguro.
Este problema de la construcción de demostraciones es NP completo. Lo que quiere decir que, si existe este algoritmo, debe servir para resolver cualquier problema en la clase \(NP\). Si este algoritmo es correcto es que \(P=NP\).
La creación artística
Alguien pensará que hablo solo de la creación matemática. Pero esencialmente es la misma situación. Pensemos en Mozart de chico, su padre, músico de profesión, daba clases de música a su hermana mayor, Mozart siendo todavía un bebé escuchaba a su padre, y veía a su hermana, tocando al piano melodías, escalas… No es sorprendente que estas melodías entraran en su cabeza, y encontraron además la mente de un niño, completamente plástica. Otro quizás habría aborrecido la música, pero él no era forzado en lo más mínimo y su mente se conformó para la música. Es el mismo proceso que indiqué antes, uno empieza por leer matemáticas y apreciar la belleza de las demostraciones, en un momento dado las ideas matemáticas y las pruebas empiezan a hervir, a bullir, formando nuevas combinaciones. La principal diferencia es que de lo que es una prueba matemática tenemos una definición precisa, de lo que es una melodía, nuestra idea no está tan bien formada. Pero, si uno lo piensa, incluso los estilos musicales son como diferencias en la definición de lo que sería una melodía perfecta.
Creo que cualquiera puede hacer matemáticas, o hacer música, o escribir. El problema es que lo primero que se necesita es motivación. Una motivación que tiene que ser profunda. La mayor parte de las personas tienen simplemente otras motivaciones. El caso de Mozart es especial, como cualquier otro caso lo sería.
El proceso que está sucediendo ahora con el programa Lean es parecido al que sucede en la mente de un matemático que está formándose. En 10 o 20 años sabremos si el proceso queda en ese punto o los ordenadores serán capaces de crear matemática. Kevin Buzzard es escéptico, pero Christian Szegedy, que es prominente en el área de Inteligencia Artificial, piensa que en 10 años los ordenadores vencerán a los matemáticos demostrando teoremas.
Para saber más.
Las dos entradas de Scholze en Xena project: Liquid tensor experiment; Half a year of the Liquid Tensor Experiment: Amazing developments.
Información sobre Lean tenemos en: Conferencia de Kevin Buzzard sobre Lean. (En el minuto 35 en adelante habla de la posibilidad de que los ordenadores encuentren demostraciones matemáticas.)
El que quiera aprender Lean, para poder usarlo quizás puede comenzar con Starting with lean.
Kevin Buzzard también explica el problema \(P=NP\) en conexión con estas ideas: Conferencia de Kevin Buzzard presentando \(P\ne NP\).
La conferencia de Feynman, Richard Feynman, pueden pensar las máquinas o La conferencia completa. Feynman comparte mi idea de que no hay genios.
Encontramos en la red diversas exposiciones sobre el experimento Scholze-Buzzard: Articulo en Nature sobre el experimento Scholze-Buzzard, o también en quanta magazine.
La imagen destacada la he tomado de la entrada de Scholze, quizás representando al monstruo de su demostración.
Dejar una contestacion