Muere con solo 51 años Vladimir Voevodsky, un prodigio de las matemáticas que dedicó su vida a un programa de detección de errores.
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.
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?
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
ta
mpoco 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.
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.
No hay comentarios:
Publicar un comentario