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¡±.