En un reciente viaje en tren de Lyon a París, Vladimir Voevodsky se sentó junto a Steve Awodey e intentó convencerlo de que cambiara su manera de hacer matemáticas.
Voevodsky, de 48 años, es miembro permanente del cuerpo docente del Institute for Advanced Study (IAS) en Princeton, Nueva Jersey. Nació en Moscú, pero habla un inglés casi perfecto y tiene la seguridad de quien no necesita demostrarle nada a nadie. En 2002 ganó la Medalla Fields, considerada a menudo el premio más prestigioso de las matemáticas.
Ahora, cuando el tren se acercaba a la ciudad, Voevodsky sacó su computadora portátil y abrió un programa llamado Coq, un asistente de demostración que ofrece a los matemáticos un entorno para escribir argumentos matemáticos. Awodey, matemático y lógico de la Carnegie Mellon University en Pittsburgh, Pensilvania, siguió el proceso mientras Voevodsky escribía la definición de un objeto matemático mediante un nuevo formalismo que había creado, llamado fundamentos univalentes. Voevodsky tardó 15 minutos en escribir la definición.
«Estaba intentando convencer a [Awodey] de que hiciera [sus matemáticas en Coq]», explicó Voevodsky durante una conferencia el otoño pasado. «Intentaba convencerlo de que es fácil hacerlo».
Para leer el resto de este artículo, visite Quanta Magazine. La publicación no implica que el Foro Económico Mundial respalde estas opiniones.
Para mantenerse al día con Agenda, suscríbase a nuestro boletín semanal.
Autor: Kevin Hartnett. Kevin escribe la columna Brainiac para la sección Ideas del Boston Globe.
Imagen: Se ve la tecla «End» de un teclado de computadora. REUTERS/Kacper Pempel.
