Adiós al matemático que buscaba errores escondidos

Solemos presumir de que las verdades matemáticas son eternas. A diferencia de otras disciplinas, en las que las teorías consideradas correctas pueden ser refutadas a la vista de nuevos resultados, los matemáticos, cuando demostramos un teorema, sabemos que será válido para siempre. Pero en la práctica, cuando terminamos de escribir la demostración, siempre existe la duda: ¿habrá algún error en los razonamientos? Nuestro sistema de publicación y difusión de los resultados establece varios filtros que ha de pasar el texto antes de que sea considerado correcto y se incorpore a la literatura científica: repasamos el trabajo con detalle; se lo explicamos a colegas, tratando de convencerles de su validez; exponemos nuestros resultados en internet donde todos los matemáticos puedan verlos; y mandamos el artículo a una revista científica en la que el editor, antes de publicarlo, lo envía a algún experto en el área, cuya labor es comprobar que no hay errores, además de evaluar si el resultado es suficientemente interesante para su publicación. Sin embargo, aunque pueda resultar inquietante, estos procesos no son infalibles, y a veces dejan pasar resultados incorrectos.

En 1998, el matemático Carlos Simpson se topó con uno de ellos. Un teorema que había enunciado en 1989 Vladmir Voevodsky no podía ser cierto, pues había encontrado un complicadísimo ejemplo donde no se satisfacía. La demostración de Voevodsky era tan técnica que Simpson tampoco fue capaz de encontrar el fallo que habían pasado por alto los revisores en su momento. Durante mucho tiempo no se sabía qué era erróneo, si la demostración de Voevodsky o el contraejemplo de Simpson, hasta que el propio Voevodsky localizó el fallo en su razonamiento en 2013. En el año 2000 encontraron otro error en otro de sus trabajos, que desde su publicación en 1993 había sido estudiado y dado por válido por los expertos.

Esto produjo una profunda impresión en Voevodsky, considerado uno de los grandes matemáticos de su generación, experto en geometría algebraica abstracta y receptor de una medalla Fields en 2002. Entonces, decidió abandonar por el momento su investigación habitual y dedicarse a buscar una manera de comprobar automáticamente los razonamientos matemáticos para detectar los errores escondidos en las demostraciones, que amenazaban con agujerear el sólido edificio de las matemáticas.

Durante mucho tiempo no se sabía qué era erróneo, si la demostración de Voevodsky o el contraejemplo de Simpson

En principio cualquier demostración se puede escribir, partiendo de unas hipótesis y siguiendo unas reglas lógicas bien definidas, de manera que una máquina podría comprobar la validez de cada paso. En la práctica esto no es posible, pues las hipótesis donde se fundamentan las matemáticas son la teoría de conjuntos, y ésta está tan alejada del tipo de argumentos que se emplean en la investigación actual, que formalizar una demostración hasta el último detalle sería un trabajo ímprobo imposible de realizar. Pero, ¿y si existiera otra teoría en la que se pudieran fundamentar las matemáticas y con la que sí fuera factible escribir demostraciones que una máquina pudiera comprobar?

Ya ha habido avances en esta dirección, sustituyendo la teoría de conjuntos por la teoría de tipos, siguiendo ideas que provienen de la informática teórica. En 2012, el equipo liderado por Georges Gonthier culminó una demostración que un ordenador puede comprobar del teorema de Feit-Thompson, un importante resultado de teoría de grupos de 1963. Voevodsky incorporó ideas de topología y geometría algebraica en la teoría de tipos.

Si se consiguiera avanzar hasta conseguir un sistema suficientemente sencillo, como para que los matemáticos lo usáramos en nuestro trabajo habitual, será una auténtica revolución. Además de evitar el problema de los errores escondidos, liberaría del arduo trabajo de comprobación y revisión al colectivo matemático. Y solucionaría situaciones como la del matemático Shinichi Mochizuki y su supuesta demostración de la llamada conjetura ABC, que la comunidad científica, a pesar de sus esfuerzos, no es capaz de validar. Por otro lado, estas ideas también se podrían usar para comprobar que los programas informáticos no contienen errores que provoquen fallos en los sistemas.

Nacido en 1966 en Moscú, Voevodsky fue un joven prodigio que enseguida llamó la atención de sus profesores. Tras la caída del muro de Berlín, hizo el doctorado en Harvard y obtuvo una plaza permanente en el prestigioso Institute for Advanced Studies, en Princeton. Su investigación se centraba en el uso de ideas de topología para estudiar problemas de la geometría algebraica. En ese campo resolvió ciertas conjeturas en álgebra, las llamadas conjeturas de Milnor y de Bloch-Kato, de gran interés para la comunidad. En 2002 obtuvo la medalla Fields, uno de los más prestigiosos premios en matemáticas. Consiguió dar pasos significativos en su programa de detección de errores pero, ni mucho menos, llegar a la refundamentación completa que buscaba. El pasado 30 de septiembre, con tan solo 51 años, fallecía en Princeton. Esperamos que su visión y su empeño prevalezcan y, al hilo de sus ideas, pueda llegarse a la revolución que él perseguía.

Tomás Gómez es investigador del Instituto de Ciencias Matemáticas (ICMAT).

Café y Teoremas es una sección dedicada a las matemáticas y al entorno en el que se crean, coordinado por el Instituto de Ciencias Matemáticas (ICMAT), en la que los investigadores y miembros del centro describen los últimos avances de esta disciplina, comparten puntos de encuentro entre las matemáticas y otras expresiones sociales y culturales, y recuerdan a quienes marcaron su desarrollo y supieron transformar café en teoremas. El nombre evoca la definición del matemático húngaro Alfred Rényi: “Un matemático es una máquina que transforma café en teoremas”.