Ads-728

Ads-728

Psicología

Astrofísica

Genética

Neurociencia

» » Para una nueva redefinición de los fundamentos de las matemáticas

Referencia: Quanta Magazine.org .
"Will Computers Redefine the Roots of Math?"
por Kevin Hartnett, 19 de mayo 2015
 * * * * * *
Después de descubrir un error en su propio trabajo, un famoso matemático se embarcó en una búsqueda por computador para eliminar el error humano. Para conseguirlo, ha de enfrentarse con la tarea de reescribir las reglas centenarias que subyacen a toda las matemáticas.

crédito Hannes Hummel para Quanta Magazine.org

En un reciente viaje en tren de Lyon a París, Vladimir Voevodsky, sentado junto con Steve Awodey, trataba de convencerle de cambiar la forma en que hace las matemáticas.

Voevodsky, de 48 años, es miembro de la facultad permanente del Instituto de Estudios Avanzados (IAS) en Princeton, Nueva Jersey. Nació en Moscú pero habla muy bien inglés, y tiene el suficiente bagaje y confianza de alguien que no tiene la necesidad de probarse a sí mismo ante cualquiera . En 2002 ganó la Medalla Fields, considerada el premio más prestigioso en matemáticas.

Cuando el tren se acercaba a la ciudad, Voevodsky sacó su portátil y abrió un programa llamado Coq, un asistente de pruebas que proporciona a los matemáticos un entorno en el que escribir argumentos matemáticos. Awodey, un matemático y lógico en la Universidad Carnegie Mellon, en Pittsburgh, a quien Voevodsky le escribió una definición de un objeto matemático usando un nuevo formalismo creado por él, llamado fundamentos univalentes. Tardó 15 minutos en escribir la definición.

"Estaba tratando de convencer a Awodey para hiciera sus matemáticas en Coq", explicaba Voevodsky durante una conferencia el otoño pasado. "Intentaba convencerle, eso es fácil de hacer."

La idea de hacer matemáticas en un programa como Coq tiene una larga historia. La apelación es simple: en lugar de confiar en lo falible de un ser humano para revisar las pruebas, se puede dar ese trabajo a los ordenadores, que pueden decirnos si las pruebas son correctas con plena certeza. A pesar de esta ventaja, los asistentes de pruebas de las computadoras no tienen adaptadas ampliamente todas las matemáticas. Esto se debe, principalmente, porque la traducción de las matemáticas a términos computacionales es engorroso y, a los ojos de muchos matemáticos, no vale la pena el esfuerzo.

Durante casi una década, Voevodsky ha estado abogando por las virtudes de los asistentes de pruebas de informática, y ha desarrollado los fundamentos univalentes con el fin de acercar el lenguaje de las matemáticas y el de la programación de computadoras. Tal como él lo ve, el paso a la formalización en el ordenador resulta necesario, porque algunos ramas de las matemáticas se han vuelto demasiado abstractas para que puedan ser revisadas de forma fiable por personas.

"El mundo de las matemáticas es cada vez más grande y su complejidad cada vez más alta, y existe la amenaza de una acumulación de errores", reseñó Voevodsky. Las pruebas se basan en otras pruebas; si una contiene un defecto, todos los demás compartirán el error.

Esto es algo que Voevodsky ha aprendido a través de su experiencia personal. En 1999 se descubrió un error en un artículo que escribió hacía siete años. Voevodsky encontró finalmente la manera de salvar el resultado, aunque en un artículo del verano pasado en el IAS newsletter, escribió sobre el susto de esa experiencia. Comenzó a preocuparse de que a poco que formalizara su trabajo en un ordenador, no podría tener plena confianza de su corrección.

Se va apuntando los pasos necesarios que él requiere repensar sobre los conceptos básicos de las matemáticas. Los fundamentos aceptados de las matemáticas es la teoría de conjuntos. Como cualquier sistema fundamental, la teoría de conjuntos proporciona un conjunto de conceptos y reglas básicas para ser utilizados en la construcción del resto de las matemáticas. La teoría de conjuntos, como fundamento, ha sido suficiente durante más de un siglo, pero no puede traducirse fácilmente a términos computacionales pueden utilizarlos en las pruebas de verificación. De ahí su decisión de iniciar la formalización de las matemáticas en los computadores, fue eso lo que puso en marcha un proceso de descubrimiento en Voevodsky que, en última instancia, le condujo a algo mucho más ambicioso: una refundación de los cimientos de las matemáticas.

La teoría de conjuntos y una paradoja

La teoría de conjuntos surgió a partir de un impulso por poner las matemáticas sobre unos asientos enteramente rigurosos --una base lógica aún más segura que los mismos números. La teoría de conjuntos comienza con un conjunto que no contiene nada, el conjunto vacío, que se utiliza para definir el número cero. El número 1 se puede construir mediante la definición de un nuevo conjunto con un elemento. El número 2 es un conjunto que contiene dos elementos, el conjunto vacío (0), y el conjunto que contiene el conjunto vacío (1). De esta forma, cada número entero se puede definir como un conjunto de conjuntos ya contenidos antes.

La teoría de conjuntos construye todas las matemáticas, comenzando con literalmente con el conjunto vacío que se define como cero.. -Olena Shmahalo/Quanta Magazine
Una vez que los números enteros están en su sitio, las fracciones se pueden definir como pares de números enteros, los decimales pueden definirse como secuencias de dígitos, las funciones en un plano como conjuntos de pares ordenados, y así sucesivamente. "Se acaba así con las estructuras complicadas, que se cuentan como un conjunto de cosas, en un conjunto de cosas, en un conjunto de cosas, y así todo el camino hasta llegar al meollo, el conjunto vacío de fondo", explicaba Michael Shulman, matemático de la Universidad de San Diego.

La teoría de conjuntos como fundamento incluye estos objetos básicos -conjuntos- y las reglas lógicas para la manipulación de tales conjuntos, de los cuales derivan los teoremas de las matemáticas. Una ventaja de la teoría de conjuntos como sistema fundamental es que es muy económico, cada objeto matemático que se quiera usar se construye, en definitiva, desde un conjunto vacío.

Por otro lado, puede ser tedioso codificar complicados objetos matemáticos como jerarquías elaboradas de conjuntos. Esta limitación se convierte en un problema cuando los matemáticos quieren pensar en los objetos equivalentes o isomorfos en algún sentido, no necesariamente iguales en todos los aspectos. Por ejemplo, la fracción decimal ½ y 0,5 representan el mismo número real, pero codificados en diferentes términos de conjuntos.

"Hay que construir un objeto específico y pegarlo con él", dijo Awodey. "Si quieres trabajar con un objeto diferente, pero isomorfo, tendrías que construir eso."

La teoría de conjuntos no es la única manera de hacer matemáticas. Los programas de asistencia a pruebas Coq y Agda, por ejemplo, se basan en un distinto sistema formal llamado teoría de tipos.

La teoría de tipos tiene sus orígenes en un intento por corregir un defecto crítico en las primeras versiones de la teoría de conjuntos, que fueron identificadas por el filósofo y lógico Bertrand Russell, en 1901. Russell señaló que algunos conjuntos auto contienen A como un miembro. Por ejemplo, consideremos el conjunto de todas las cosas que no son naves espaciales. Este conjunto, el conjunto no-naves espaciales, en sí mismo no es una nave espacial, así que es un miembro de sí mismo.

Russell definió un nuevo conjunto: el conjunto de todos los conjuntos que no se auto contienen. Él se preguntaba si ese conjunto se contiene a sí mismo, y demostró que responder a estas preguntas produce una paradoja: si un conjunto se contiene a sí mismo, entonces no se contiene a sí mismo (porque los únicos objetos del conjunto son los conjuntos que no se contienen a sí mismos). Pero si no se contiene a sí mismo, a su vez se contiene a sí mismo (porque el conjunto contiene todos los conjuntos que no se contienen a sí mismos).

Russell creó la teoría de tipos como una manera de salir de esta paradoja. En lugar de la teoría de conjuntos, el sistema de Russell utilizaba objetos más cuidadosamente definidos, llamados tipos. La teoría de Russell comienza con una universo de objetos, al igual que la teoría de conjuntos, y esos objetos pueden ser recogidos en un "tipo" llamado conjunto. Dentro de la teoría de tipos, el tipo ‘conjunto’ se define de tal modo que sólo permite recoger objetos que no son recogidos por otros. Si una colección contiene otras colecciones, ya no se le permite ser un ‘conjunto’, pero es algo que puede ser considerado como un Mega-conjunto, una nueva especie de tipo definido específicamente como una colección de objetos que en sí mismos son colecciones de objetos.

Desde aquí, emerge todo el sistema de una manera ordenada. Uno puede imaginar, por ejemplo, un tipo llamado Super-mega-conjunto que recoge solamente objetos que son Mega-conjuntos. Dentro de este rígido marco, se convierte en ilegal, por así decirlo, plantear siquiera la cuestión de la paradoja inducida, "¿El conjunto de todos los conjuntos que no se contienen a sí mismos, se contienen sí mismos?" En la teoría de tipos, los conjuntos contienen únicamente objetos que no son colecciones de otros objetos.

Una importante distinción entre la teoría de conjuntos y la teoría de tipos radica en la forma en que son tratados los teoremas. En la teoría de conjuntos, un teorema no es en sí mismo un conjunto, es una declaración acerca de los conjuntos. Por el contrario, en algunas versiones de la teoría de tipos, los teoremas y los conjuntos están en igualdad de condiciones. Son "tipos" -una nueva clase de objeto matemático. Un teorema es un tipo cuyos elementos son las diferentes maneras en las que el teorema se puede demostrar. Así, por ejemplo, hay un solo tipo que recoge todas las pruebas del teorema de Pitágoras.

Para ilustrar esta diferencia entre ambas teorías, consideremos dos conjuntos: el conjunto A contiene dos manzanas y el conjunto B contiene dos naranjas. Un matemático podría considerar ambos conjuntos como equivalentes, o isomorfos, porque tienen el mismo número de objetos. La manera de demostrar formalmente que estos dos conjuntos son equivalentes es emparejar los objetos del primer conjunto con los objetos del segundo. Si se emparejan uniformemente, sin objetos que sueltos que queden al margen, son equivalentes.

Al hacer este emparejamiento, vemos rápidamente que hay dos maneras de demostrar la equivalencia: la manzana 1 se puede emparejar con la naranja 1 y la manzana 2 con la naranja 2, o la manzana 1 con la naranja 2 y la manzana 2 con la naranja 1. Otra forma de decir esto, consiste en declarar que los dos conjuntos son isomorfos entre sí de dos formas.

En una prueba tradicional de la teoría de conjuntos del teorema Set A ≅ Set B (donde el símbolo ≅ significa "es isomorfo a"), los matemáticos se refieren sólo a si existe tal emparejamiento. En la teoría de tipos, el teorema Set A ≅ Set B puede ser interpretado como una colección, que consiste en todas las diferentes maneras de demostrar el isomorfismo (en este caso, dos). A menudo, en matemáticas, hay buenas razones para hacer un seguimiento de las diversas maneras en que dos objetos (como estos dos conjuntos) son equivalentes, y la teoría de tipos hace esto automáticamente agrupando equivalencias en un único tipo.

Esto es especialmente útil en topología, una rama de las matemáticas que estudia las propiedades intrínsecas de los espacios, como un círculo o el área de un dónut. Estudiar los espacios sería impracticable si los topólogos tuviesen que pensar por separado sobre todas las variaciones posibles de espacios con las mismas propiedades intrínsecas. (Por ejemplo, los círculos pueden ser de cualquier tamaño, sin embargo, cada círculo comparte las mismas cualidades básicas). Una solución es reducir el número de espacios diferenciados considerando algunos de ellos como equivalentes. Una forma de hacer esto es con la noción de homotopía, la cual proporciona una definición útil de la equivalencia: Los espacios tienen homotopía equivalente si, en términos generales, puede deformarse dentro de otro por contracción, o regiones espesantes, sin desgarrarse.

El punto y la línea tienen homotopía equivalente, que es otra forma de decir que tienen un mismo tipo de homotopía. La letra P tiene el mismo tipo de homotopía que la letra O (la cola de la P puede plegarse hacia el mismo límite del círculo superior de la letra), y la P y la O tienen la misma homotopía que las otras letras del alfabeto que contienen un agujero, la A, D, Q y la R.

Los tipos de homotopía se usan para clasificar las características esenciales de un objeto. Las letras A, R y Q tienen todas un agujero, así que todas tienen el mismo tipo de homotopía. Las letras C, X y K tienen también el mismo tipo de homotopía, todas ellas pueden transformarse en una línea.

Los topólogos usan diferentes métodos para evaluar las cualidades de un espacio y determinar sus tipos de homotopía. Una de ellos es el estudio de la colección de vías entre distintos puntos en el espacio, y la teoría de tipos es muy adecuada para hacer el seguimiento de estas vías. Por ejemplo, un topólogo podría pensar en dos puntos en un espacio como equivalentes siempre que haya una vía que los conecte. Entonces, la colección de todos las vías entre los puntos x e y pueden, en sí misma, ser vista como un tipo simple, lo que representa todas las pruebas del teorema x = y.

Pueden construirse tipos de homotopía puede a partir de vías entre puntos, pero el emprendedor matemático  puede mantener un seguimiento de las vías entre vías, y entre vías, y así sucesivamente. Estas vías entre vías pueden entenderse como relaciones de orden superior entre puntos en un espacio.

Voevodsky trató este asunto de manera intermitente durante 20 años, comenzó cuando estudiante en la Universidad Estatal de Moscú a mediados de la década de 1980, para formalizar las matemáticas de manera que crearía relaciones de orden superior --vías de vías de vías- fáciles de trabajar. Al igual que muchos otros durante este período, trató de conseguir esto dentro del marco de un sistema formal llamado teoría de categorías. Y mientras que lograba un éxito limitado en el uso de la teoría de categorías a la hora de formalizar áreas particulares de las matemáticas, había áreas de las matemáticas que las categorías que no podían alcanzar.

Voevodsky retomó el problema de estudiar las relaciones de orden superior con un interés renovado, en los años posteriores a ganar la Medalla Fields. A finales de 2005, sintió una especie de epifanía. Tan pronto como comenzó a pensar acerca de las relaciones de orden superior en términos de objetos llamados grupoides infinitos, dijo que, "muchas cosas empezaron a encajar en su lugar."

Los grupoides infinitos codifica todos las vías de un espacio, incluidas las vías de vías de vías. Estos surgen en otras fronteras de la investigación matemática como formas de codificación de similares relaciones de orden superior, aunque son objetos difíciles de manejar desde el punto de vista de la teoría de conjuntos. Debido a esto, se cree que son inútiles, al menos para el objetivo de Voevodsky de formalizar las matemáticas.

No obstante, Voevodsky fue capaz de crear una interpretación de la teoría de tipos al lenguaje de grupoides infinitos, un avance que permite a los matemáticos razonarlos de manera eficiente sin tener que pensarlos en términos de conjuntos. Este avance, en última instancia, ha conducido a la elaboración de los fundamentos univalentes.

Voevodsky se sentía emocionado por el potencial de un sistema formal construido sobre grupoides, aunque el objetivo intimidaba por la cantidad de trabajo técnico requerido para realizar esta idea. Le preocupaba que cualquier progreso se hiciera demasiado complicado a la hora de ser verificado fiablemente a través de una revisión por pares, por lo cual Voevodsky llegó a comentar en aquel momento que estaba "perdiendo la fe".

Hacia un nuevo sistema

Con los grupoides, Voevodsky tenía su objeto, lo que le dejaba necesitado solamente de un marco formal donde organizarlo. En 2005, lo encontró en un artículo inédito llamado “Folds”, que introdujo a Voevodsky en un sistema formal que encajaba asombrosamente bien con la clase de orden superior matemático que quería practicar.

En 1972, el lógico sueco Per Martin-Löf presentó su propia versión de la teoría de tipos, inspirado en las ideas de Automath, un lenguaje formal para el control de pruebas en el computador. La teoría de tipos (MLTT) de Martin-Löf fue ansiosamente adoptada por los informáticos, quienes lo han utilizado como base para los programas de asistencia a pruebas.

A mediados de 1990, la MLTT se cruzó con la matemática pura de la mano de Michael Makkai, un especialista en lógica matemática que se retiró de la Universidad McGill en 2010, al darse cuenta que podría ser utilizada para formalizar categorías y categorías de orden superior matemáticas. Voevodsky dijo que cuando leyó por primera vez la obra de Makkai, describiendo los ‘Folds’, la experiencia fue "casi como un hablar conmigo mismo, en el buen sentido."

Los fundamentos univalentes de Vladimir Voevodsky tienen el objetivo de reconstruir las matemáticas de manera que permita a los ordenadores testear todas las pruebas matemáticas. Andrea Kane/Institute for Advanced Study

Los fundamentos univalentes de Vladimir Voevodsky tienen el objetivo de reconstruir las matemáticas de manera que permita a los ordenadores testear todas las pruebas matemáticas. Voevodsky siguió las vías de Makkai, pero usando grupoides en lugar de categorías. Esto le permitió crear profundas conexiones entre la teoría de la homotopía y la teoría de tipos.

Voevodsky señalaba que dicha conexión es mágica, aunque su significancia es un tanto distinta. Para él, el potencial real de la teoría de tipos, informada por la teoría de homotopía, da lugar a  una nueva fundamentación de las matemáticas excepcionalmente bien adaptada a la computación. Tanto para la verificación como para el estudio de las relaciones de orden superior.

Voevodsky se percató primero de esta conexión cuando leyó el artículo de Makkai, pero aún tardó cuatro años para que hacerlo matemáticamente preciso. De 2005 a 2009 desarrolló varias piezas de una maquinaria que permitía a los matemáticos trabajar con conjuntos de MLTT, "de forma consistente y conveniente por primera vez", dijo. Esto incluye un nuevo axioma, conocido como el axioma univalente, y una completa interpretación de MLTT al lenguaje de conjuntos simplicial que, además de grupoides, otra forma de representación de tipo de homotopía.

Esta consistencia y conveniencia refleja algo más profundo sobre el programa, dijo Daniel Grayson, profesor emérito de matemáticas en la Universidad de Illinois en Urbana-Champaign. La fuerza de los fundamentos univalentes radica en el hecho de que se nutre de una estructura anteriormente ocultas en las matemáticas.

"Lo que hace atractivo y diferente a las fundamentos univalentes, especialmente si se intenta reemplazar a la teoría de conjuntos", dijo, "es que las ideas de la topología se avienen muy bien con los fundamentos de las matemáticas."

De la idea a la acción

La construcción de nuevos fundamentos para las matemáticas es una cosa. Hacer que la gente lo utilice es otra. A finales de 2009, Voevodsky ya había sacado los detalles de los fundamentos univalentes y se sintió preparado para empezar a compartir sus ideas. Él entendía que la gente probablemente se mostrara escéptica. "Es una gran cosa esto de decir que tengo algo que probablemente pueda reemplazar la teoría de conjuntos."

Voevodsky primero discutió los fundamentos univalentes públicamente en una conferencia en el Carnegie Mellon a principios de 2010 y en el Instituto de Investigación Oberwolfach de Matemática en Alemania, en 2011. En las charlas en Carnegie Mellon se reunió con Steve Awodey, que había seguido la investigación con sus alumnos de posgrado Michael Warren y Peter Lumsdaine, sobre la teoría de la homotopía. Poco después, Voevodsky decidió reunirse con los Investigadores para una cooperación intensiva a fin de poner en marcha el desarrollo del campo.

Junto con Thierry Coquand, un científico informático de la Universidad de Gotemburgo, en Suecia, Voevodsky y Awodey organizaron un año de investigación especial para asumirlo en IAS durante el año académico 2012-2013. Más de una treintena de científicos informáticos, lógicos y matemáticos llegaron de alrededor del mundo para participar. Voevodsky les dijo que sus ideas resultarían extrañas al principio, "no había ni una sola persona allí que se sintiera cómoda con él."

Las ideas pudieron ser un poco extrañas, pero el objetivo emocionante. Shulman aplazó el inicio de un nuevo trabajo con el fin de tomar parte del proyecto. "Creo que muchos de nosotros nos sentíamos en la cúspide de algo grande, algo realmente importante", comentó, "y que valió la pena hacer sacrificios y estar involucrado en la misma génesis del asunto."

Tras el año de investigación especial, la actividad se dividió en unas pocas direcciones distintas. Un grupo de investigadores, entre ellos Shulman y la llamada comunidad HoTT (para teoría de tipos de homotopía), y explorar las posibilidades de nuevos descubrimientos desarrollados en ese marco. Otro grupo, identificado como UniMath, donde se incluía Voevodsky, reescribía la matemáticas en el lenguaje de los fundamentos univalentes. Su objetivo es crear una biblioteca de elementos matemáticos básicos —lemas, pruebas, proposiciones— que los matemáticos pueden usar para formalizar su propio trabajo de fundamentos univalentes.

Conforme las comunidades HoTT y UniMath han ido  creciendo, las ideas que subyacen a ellos se han ido haciendo más visibles entre los matemáticos, lógicos y científicos informáticos. Henry Towsner, un lógico de la Universidad de Pensilvania, decía que parecía haber al menos un tipo de presentación de la teoría de homotopía en cada conferencia que se espera dar en estos días, y que cuanto más aprende sobre el enfoque, más cobra sentido. "Ha sido palabra de moda", dijo. "Me tomó un tiempo entender lo que realmente estaban haciendo  y por qué era interesante y una buena idea, no una cosa efectista."

Gran parte de la atención de los fundamentos univalentes ha recaído en Voevodsky como uno de los más grandes matemáticos de su generación. Michael Harris, un matemático de la Universidad de Columbia, incluye larga discusión de los fundamentos univalentes en su nuevo libro, “Mathematics Without Apologies”. Él está impresionado por las matemáticas rodean el modelo univalente, pero es más escéptico que Voevodsky respecto a un mundo donde los matemáticos formalicen su trabajo en tales fundamentos y puedan comprobarlo en el ordenador.

"El deseo de mecanizar la verificación de pruebas y pruebas no es la motivación más fuerte en los matemáticos, es cuanto puedo decir", dijo. "Puedo entender por qué los informáticos y los lógicos estén entusiasmados, pero creo que los matemáticos están buscando algo más."

Voevodsky es consciente de que unos nuevos fundamentos para las matemáticas son difíciles de vender, y admite que "por el momento hay más bombo y ruido que preparación real de este campo." Actualmente está usando el lenguaje de fundamentos univalentes para formalizar la relación entre MLTT y la teoría de homotopía, que él considera un paso necesario en el desarrollo del campo. Voevodsky también planea formalizar su prueba de la conjetura de Milnor, con la cual obtuvo una Medalla Fields. Espera hacerlo para que eso pueda actuar como "un hito capaz de crear motivación en el campo."

Finalmente a Voevodsky le gustaría utilizar los fundamentos univalentes para estudiar los aspectos de las matemáticas que han sido inalcanzables dentro del marco de la teoría de conjuntos. Aunque por ahora está haciendo todo ello con cautela. La teoría de conjuntos ha afianzado las matemáticas durante más de un siglo, y si los fundamentos univalentes esperan tener una longevidad similar, Voevodsky sabe que es importante hacer las cosas bien desde el principio.

# # # # #
-

«
Next
Entrada más reciente
»
Previous
Entrada antigua
Editor del blog Pedro Donaire

Filosofía

Educación

Deporte

Tecnología

Materiales