Un teórico de los números teme que todo lo que sabemos sobre las matemáticas esté mal

El software de las matemáticas puras está infectado. Varios de los pesos pesados del campo, reconocidos por su autosuficiencia, están empezando a recurrir al software para comprender y verificar demostraciones.

Kevin Buzzard, teórico matemático y profesor de matemáticas puras en el Imperial College London, considera que ha llegado el momento de crear una nueva área de la materia dedicada a la informatización de las demostraciones, algunas de las cuales se han vuelto tan complejas que prácticamente no hay humanos capaces de entender todos sus entresijos, y mucho menos de verificarlas. Buzzard teme que muchas de las demostraciones que hasta ahora se han considerado válidas de forma generalizada en realidad sean erróneas. Se necesita ayuda.

¿Qué es una demostración? Es un argumento que se expone para justificar la verdad de un postulado matemático. Al demostrar las cosas y aprender nuevas técnicas para hacerlo, se mejora en la comprensión de las matemáticas, lo cual redunda a su vez en otros campos.

Para elaborar una demostración, se empieza con definiciones. Por ejemplo, escribimos un conjunto de números como los enteros, todos los números desde el menos infinito hasta al infinito positivo. Escribimos ese conjunto del siguiente modo: …. -2, -1, 0, 1, 2, … A continuación, proponemos un teorema; por ejemplo, que no existe el número entero más grande. La demostración, en este caso, consiste en explicar el razonamiento lógico que prueba que el teorema es cierto o falso (en este caso, cierto). Los pasos lógicos de la demostración se sustentan en otras verdades previamente aceptadas y demostradas, como por ejemplo, que el número 1 es menor que 2.

Las nuevas demostraciones expuestas por los matemáticos profesionales suelen basarse en resultados anteriores, ya publicados y asimilados. Lo que Buzzard sugiere es que, en muchos casos, no se han entendido esas demostraciones anteriores sobre las que se han construido las nuevas. Como ejemplo, cita varios artículos destacados en los que se hace alusión abiertamente a trabajos no publicados. Este es el aspecto que preocupa a Buzzard.

“Me ha sobrevenido la preocupación de que toda la matemática publicada sea errónea por falta de verificación de los detalles por parte de los expertos. No sería la primera vez que veo errores”, nos dijo Buzzard en una entrevista durante la 10 Conferencia Interactiva para la Demostración de Teoremas de Portland, Oregón, en la que dio la charla inaugural.

“Creo que existe una posibilidad diferente a cero de que hayamos construido algunos de nuestros grandes castillos en la arena”, señaló en una presentación. “Pero considero que es muy pequeña”.

Se supone que las nuevas matemáticas están demostradas desde su base. Cada paso debe ser comprobado, o al menos debe haberse seguido el razonamiento que lo sustenta. Por otro lado, hay expertos y eruditos de la comunidad de matemáticos que ofrecen una guía testimonial fiable sobre lo que es y no es cierto. Si un erudito cita un artículo en su obra, según esta lógica, se da por sentado que dicho artículo se ha verificado.

Buzzard sugiere que las matemáticas modernas dependen demasiado de la palabra de los eruditos porque los resultados son demasiado complejos. En una nueva demostración pueden llegar a citarse a otros 20 artículos, algunos de los cuales constan de 1000 páginas de denso razonamiento. Si un matemático respetado citara o basara su axioma en uno de esos artículos de 1000 páginas, muchos otros matemáticos se limitarían a aceptar la veracidad tanto de lo postulado en dicho documento como de la nueva demostración, sin tomarse la molestia de verificarlo. Pero se supone que las matemáticas han de ser demostrables universalmente y que no deben depender de un puñado de expertos.

Este exceso de confianza confiere cierto grado de fragilidad al proceso de comprensión de la verdad. En la década de 1990, se publicó una demostración del Último Teorema de Fermat, postulado en 1637 y en su momento calificado como el “problema matemático más complicado del mundo” por el Libro Guinness de los Récords. Buzzard sostiene que en realidad nadie lo entiende por completo ni es capaz de determinar si es cierto.

“Ningún ser humano, vivo o muerto, conoce todos los detalles de la demostración del Último Teorema de Fermat. Pese a ello, la comunidad lo ha aceptado”, escribió Buzzard en una presentación. Porque “los eruditos han decretado que la demostración es válida”.

Hace un par de años, Buzzard acudió a charlas impartidas por los avezados matemáticos Thomas Hales y Vladimir Voevodsky, gracias a las cuales tuvo conocimiento de la existencia de un software de verificación de demostraciones muy efectivo. Esta solución permite que un ordenador verifique demostraciones sistemáticamente, eliminando el factor humano y democratizando el estado de la verdad.

Buzzard enseguida se enganchó a este software de verificación, al que han bautizado como Lean. Este no solo permitía verificar demostraciones sin ningún atisbo de duda, sino que fomentaba una aproximación a las matemáticas clara e inequívoca.

“Me di cuenta de que los ordenadores solo aceptarían la entrada de datos muy precisos, que para mi gusto es la mejor forma de abordar las matemáticas”, dijo Buzzard. “Me enamoré, porque tuve la sensación de haber encontrado un alma gemela. Había encontrado algo que procesaba las matemáticas del mismo modo que lo hacía yo”.

Para verificar una demostración, un usuario de Lean debe primero formalizarla, es decir, pasar su contenido del lenguaje humano y los símbolos al lenguaje de programación del software. También es preciso formalizar cualquier definición o demostración complementaria sobre la que el nuevo axioma se fundamente. Aunque este proceso de conversión es laborioso, Lean parece aguantar todo lo que le echa Buzzard, un aspecto que lo distingue de otros programas de verificación.

Lean ha llamado la atención de una creciente comunidad de matemáticos, especialmente en el ámbito de la educación. Jeremy Avigad es profesor en Carnegie Mellon y está especializado en teoría de la demostración. Tanto él como Buzzard han empezado a usar Lean en sus clases introductorias sobre demostraciones. El software comprueba la veracidad de cada una de las líneas de una demostración y genera un informe que resulta muy útil para los alumnos.

Pese a su entusiasmo ante el interés que ha generado Lean en la comunidad, Avigad advierte de que esta tecnología todavía debe mejorar. El uso de estas soluciones requiere de mucho tiempo. “Este campo existe desde hace unas décadas y las cosas están mejorando, pero aún queda camino por recorrer”, añadió.

Buzzard cree que, si se logran superar estos escollos, el software podría tener otras aplicaciones además de las demostraciones. Pongamos el caso de la búsqueda. Cada año se publican enormes cantidades de nuevos resultados a un ritmo vertiginoso, lo cual hace de las búsquedas en estas demostraciones un aspecto de extrema importancia.

Hales y Buzzard han señalado que si se introdujeran en Lean todos los resúmenes de los nuevos trabajos, cualquier matemático podría consultar la base de datos de esos resúmenes para buscar un objeto matemático preciso y obtener toda la información que existe al respecto. Esto equivaldría, hasta cierto punto, a desnudar los cerebros de los eruditos.

Los científicos informáticos podrían usar esas bases de datos para formar IA. Como los resultados de la base de datos estarían definidos en el lenguaje preciso de Lean, un programa podría aprenderlos más fácilmente que si estuvieran escritos en inglés.

En última instancia, lo ideal para los expertos en computación sería crear una solución automatizada general que verificara teoremas, un sistema de software capaz de crear demostraciones propias, de hacer sus propios cálculos. Este tipo de soluciones se basan en la misma tecnología que Lean para determinar la veracidad de un axioma. La adopción cada vez más generalizada de Lean puede constituir un paso necesario hacia la automatización global de las matemáticas.

Michael Harris, profesor de matemáticas de la Universidad de Columbia y compañero de Buzzard, teme que el resto de la comunidad científica y las empresas tecnológicas dispuestas a automatizar las matemáticas no compartan las mismas motivaciones que los matemáticos. A los expertos en computación, por ejemplo, les interesa usar usar la tecnología de Lean para comprobar que sus programas no tienen fallos. Las empresas buscan beneficios. Y los matemáticos como Buzzard lo único que quieren es dedicarse a lo suyo, las matemáticas.

“Lo que puedo predecir es que, si expertos con talento como Thomas Hales y Buzzard continúan con esa línea de pensamiento, saldrá algo muy interesante de todo esto; tal vez no sea una IA, pero sí nuevas ramas de las matemáticas o nuevas formas de pensar”, señaló Harris.