Una pequeña comunidad de matemáticos está utilizando Lean para construir una nueva base digital. Esperan que asegure el futuro de su campo científico.
Todos los días, decenas de matemáticos de ideas afines se reúnen en el chat de Zulip para trabajar en lo que creen que dará forma al futuro de su campo científico.
Todos son fanáticos del programa Lean . Es una herramienta interactiva de demostración de teoremas que, en principio, es capaz de ayudar a los matemáticos a escribir pruebas. Sin embargo, para esto, los matemáticos deben ingresar manualmente reglas matemáticas en la base del programa, llevando el conocimiento recolectado durante miles de años a una forma comprensible para una computadora.
Para muchos participantes en el proyecto, sus beneficios requieren poca o ninguna explicación.
"En un nivel fundamental, es obvio que una vez que algo se digitaliza, se puede utilizar de nuevas formas", dijo Kevin Buzzard.del Imperial College de Londres. "Y vamos a digitalizar las matemáticas para mejorarlas".
Digitalizar las matemáticas es un viejo sueño. Los beneficios esperados de esto van desde lo trivial (verificar la tarea de los estudiantes con computadoras) hasta lo extraordinario: usar inteligencia artificial para hacer nuevos descubrimientos matemáticos y encontrar nuevas soluciones a viejos problemas. Los matemáticos creen que los probadores automáticos de teoremas también podrán revisar artículos enviados a revistas, encontrar errores que los revisores humanos a veces pasan por alto y participar en el tedioso trabajo técnico de completar la prueba con todos los detalles necesarios.
Pero primero, los matemáticos que se reúnen en una charla deben equipar a Lean con conocimientos dentro del marco de las matemáticas escolares, y hasta ahora esta tarea solo está a medio completar. En un futuro cercano, es poco probable que Lean pueda resolver problemas abiertos, pero las personas que trabajan en la base están casi seguras de que en unos pocos años el programa al menos aprenderá a comprender los problemas de nivel de examen en la escuela secundaria.
¿Quién sabe? Los matemáticos que participan en el proyecto no siempre tienen una idea clara de para qué pueden ser útiles las matemáticas digitales.
“No sabemos exactamente a dónde vamos”, dijo Sebastien Gösel de la Universidad de Rennes.
Tu planeas, Lean funciona
Durante el verano, un grupo de usuarios experimentados de Lean realizó un seminario en línea " Lean para matemáticos curiosos ". En la primera lección, Scott Morrison de la Universidad de Sydney mostró cómo se puede escribir una prueba usando un programa.
Comenzó por escribir la declaración que quería demostrar en términos Lean. En lenguaje humano, significaba "hay un número infinito de números primos". Hay varias formas de probar esta afirmación, pero Morrison quería usar una versión ligeramente modificada de la primera evidencia encontrada por Euclides del 300 a. C. En la prueba, todos los números primos conocidos se multiplican y luego, después de sumar 1, se obtiene un nuevo número primo (el producto en sí o uno de sus divisores será primo). La elección de Morrison se basó en una de las reglas básicas para usar Lean: el usuario debe proponer él mismo la idea principal de la prueba.
"Usted es responsable de la primera suposición", dijo Morrison en una entrevista.
Después de ingresar la afirmación y elegir una estrategia, Morrison describió la estructura de la prueba en unos minutos. Identificó una secuencia de pasos intermedios, cada uno de los cuales era relativamente fácil de probar. Si bien Lean no puede ofrecer una estrategia de prueba general, puede ayudarlo a ejecutar pasos pequeños y concretos. Al dividir la prueba en subtareas accesibles, Morrison era un poco como un chef que instruye a los cocineros comunes para que piquen cebollas o hiervan agua. "Aquí es donde espera que Lean se haga cargo y lo ayude", dijo Morrison.
Lean realiza tareas intermedias mediante procesos automatizados llamados tácticas. Son una especie de algoritmos cortos diseñados para realizar tareas muy específicas.
Trabajando con pruebas, Morrison lanzó una táctica llamada búsqueda en la biblioteca. Buscó en la base de datos matemática del programa y devolvió varios teoremas que pensó que podrían llenar los vacíos en una sección particular de la demostración. Diferentes tácticas realizan diferentes tareas matemáticas. Uno de ellos, linarith, puede tomar un conjunto de desigualdades para, digamos, dos números reales, y confirmar la verdad de la nueva desigualdad, que incluye el tercer número: si a es 2 y b es mayor que a, entonces 3a + 4b es mayor que 12. El otro hace la mayor parte de la trabajar con reglas algebraicas básicas como la asociatividad.
“Hace dos años en Lean, la asociatividad tenía que aplicarse manualmente”, dijo Amelia Livingston, una estudiante de matemáticas en el Imperial College de Londres que está estudiando Lean con Buzzard. - Y luego alguien escribió una táctica que lo hace por ti. Soy feliz cada vez que lo uso ".
En total, a Morrison le tomó 20 minutos completar la prueba de Euclides. Aquí y allá él mismo completaba los detalles; a veces los tácticos lo hacían por él. Después de cada paso, Lean verificó la consistencia de la prueba de acuerdo con reglas lógicas integradas escritas en un lenguaje formal llamado teoría de tipos dependientes .
“Parece una aplicación de Sudoku. Si haces un movimiento en falso, suena un pitido ”, dijo Buzzard. Como resultado, Lean confirmó la viabilidad de la prueba de Morrison.
Fue un ejercicio muy divertido, como suele ocurrir cuando la tecnología hace algo por ti. Sin embargo, la prueba de Euclides ha existido durante más de 2000 años. Las preguntas de los matemáticos de hoy son tan complejas que Lean ni siquiera puede entenderlas, y mucho menos ayudar a responderlas.
"Probablemente se necesitarán décadas para que esta herramienta ayude con la investigación", dijo Heather Macbeth de la Universidad de Fordham, una de las usuarias de Lean.
Entonces, antes de que los matemáticos puedan trabajar con Lean en preguntas que realmente les interesen, deben agregar más reglas matemáticas al programa. Y esto, de hecho, es una tarea bastante sencilla.
Anatomía de un programa de construcción de pruebas: Lean ayuda a los matemáticos a probar teoremas al verificar el trabajo y automatizar algunos pasos de prueba.
1) El matemático describe la estructura básica de la demostración y escribe la secuencia de pasos en Lean.
2) La biblioteca de programas de matemáticas mathlib tiene un conjunto de tácticas que realizan los pasos de esta prueba. Los matemáticos siguen agregando nuevos datos a mathlib. Los teoremas probados se agregan a mathlib.
3) El algoritmo Kernel verifica la exactitud de la demostración usando reglas simples.
* El pulpo se ha convertido de alguna manera en la designación de las emociones alegres en la comunidad Lean.
“Para que Lean pueda entender algo, la gente necesita traducir los libros de texto de matemáticas a una forma que el programa pueda entender”, dijo Morrison.
Desafortunadamente, la simplicidad de un problema no significa que sea fácil de completar, dado que gran parte de las matemáticas no se tratan en los libros de texto.
Conocimiento disperso
Si no ha estudiado matemáticas avanzadas, esta área puede parecerle precisa y bien descrita. Álgebra, cálculo diferencial, análisis matemático: todo se deriva de todo y hay respuestas a todas las preguntas, que se enumeran al final del libro de texto.
Sin embargo, las matemáticas en el plan de estudios de la escuela, el plan de estudios universitario e incluso gran parte de la universidad son una parte muy pequeña de todo el conocimiento. La mayoría de ellos no están bien organizados.
Hay áreas enormes e importantes de las matemáticas que no se describen completamente. Están almacenados en la mente de un pequeño número de personas que aprendieron su subcampo de las matemáticas de personas que lo aprendieron de quienes lo inventaron; es decir, existen sobre la base del folclore.
Hay otras áreas donde se registra el material básico, pero es tan complejo y largo que nadie ha podido verificar su exactitud. En cambio, los matemáticos simplemente creen en él.
“Confiamos en la reputación del autor. Sabemos que es un genio y un tipo meticuloso, por lo que la prueba probablemente sea cierta ”, dijo Patrick Massot de la Universidad de Paris-Saclay.
Ésta es una de las razones por las que los programas de demostración de teoremas son tan atractivos. Traducir las matemáticas a un lenguaje comprensible para una computadora obliga a los matemáticos a catalogar finalmente sus conocimientos y definir con precisión todos los objetos.
Assia Mabubidel Instituto Estatal Francés de Investigación en Ciencias de la Computación y Automatización recuerda la primera vez que se dio cuenta del potencial de una biblioteca digital tan ordenada: “Me cautivó la posibilidad de una cobertura teórica de toda la literatura matemática utilizando el lenguaje de la lógica pura, almacenando toda la biblioteca matemática en una computadora, verificando y buscando datos en ella con la ayuda de programas ".
Lean no es el primer programa que tiene este potencial. El primero, Automath, apareció en la década de 1960, y Coq, uno de los más populares en la actualidad, salió en 1989. Los usuarios de Coq formalizaron muchas matemáticas en lenguaje de programa, pero este trabajo estaba descentralizado y no estaba bien organizado. Los matemáticos trabajaron solo en proyectos que les interesaban e identificaron solo aquellos objetos que necesitaban para su propio trabajo, a menudo describiéndolos de maneras únicas. Como resultado, las bibliotecas de Coq se ven desordenadas, como el plano de una ciudad que creció de forma natural.
“Coq es un anciano con cicatrices hoy”, dijo Mabubi, quien ha estado activo en el programa. "Fue apoyado por muchas personas durante mucho tiempo, y gracias a su dilatada trayectoria, sus defectos ahora son bien conocidos".
En 2013, Leonardo de Mura , investigador de Microsoft, lanzó el proyecto Lean. Su nombre [lean] refleja el deseo de De Moore de crear un programa eficiente y limpio. Supuso que el programa sería una herramienta para verificar la precisión del código de otros programas, no matemática. Sin embargo, resulta que verificar la exactitud de un programa es muy parecido a verificar una prueba.
“Creamos Lean porque estamos interesados en el desarrollo de software, y existe una analogía entre crear matemáticas y escribir código”, dijo de Moore.
Heather Macbeth de la Universidad de Fordham, una de las usuarias de Lean
En el momento del lanzamiento de Lean, había bastantes otros programas de ayuda, incluido Coq, que es más similar a Lean. La base lógica de ambos programas se basa en la teoría de tipos dependientes. Sin embargo, Lean ofrece la oportunidad de empezar de nuevo.
Rápidamente atrajo a los matemáticos. Lo utilizaron con tal entusiasmo que comenzaron a tomar todo el tiempo libre de De Moore con sus preguntas sobre el desarrollo en el campo de las matemáticas. "Se cansó un poco de los principales matemáticos y dijo: ¿por qué no hacen un depósito separado?" Dijo Morrison.
Los matemáticos crearon esta biblioteca en 2017. Lo llamaron mathlib y celosamente se dispusieron a llenarlo con conocimiento matemático mundial, creando algo así como un análogo de la Biblioteca de Alejandría.en el siglo XXI. Los matemáticos crearon y cargaron fragmentos de matemáticas digitalizadas, creando gradualmente un catálogo para Lean. Y dado que mathlib era nuevo, podían aprender de las limitaciones de sistemas anteriores como Coq y realizar un seguimiento de cómo estaba organizado el material.
"Hay un intento deliberado de crear una biblioteca matemática monolítica, cuyos fragmentos funcionarán entre sí", dijo Macbeth.
Mathlib alejandrino
La página de inicio del proyecto mathlib tiene gráficos que muestran el progreso del proyecto en tiempo real. El proyecto tiene una lista de líderes que más invierten en él, ordenados por el número de líneas de código [en primer lugar, por cierto, está el matemático ruso Yuri Kudryashov / aprox. transl.]. También se calcula el número total de objetos matemáticos digitalizados: a principios de octubre, contiene 18.756 definiciones y 39.157 teoremas.
Todos estos ingredientes de las matemáticas se pueden mezclar para crear matemáticas dentro de Lean. Hasta ahora, su rango es muy limitado, a pesar de los números aparentemente impresionantes. No hay casi nada de áreas de análisis complejo o ecuaciones diferenciales, y estos son dos elementos básicos de muchas áreas de las matemáticas superiores. Además, el programa aún no sabe lo suficiente como para describir ninguno de los Problemas del Milenio, problemas matemáticos definidos por el Clay Mathematical Institute en 2000 como "problemas clásicos importantes que no se han resuelto durante muchos años".
mathlib se está completando lenta pero seguramente. El trabajo se desarrolla con espíritu de trabajo en equipo. En el chat de Zulip, los matemáticos seleccionan las definiciones que requieren formalización, se les pide que las anoten y brinden pronta retroalimentación sobre el trabajo de otros.
“Cualquier matemático investigador puede estudiar Mathlib y hacer una lista de 40 cosas que no existen”, dijo Macbeth. - Por eso decide suplir alguna de estas deficiencias. Y el placer instantáneo está garantizado: alguien leerá tu trabajo y dejará un comentario al respecto en 24 horas ".
Muchos complementos resultan pequeños, como descubrió Sophie Morelde la Escuela Normal de Lyon durante el seminario en línea "Lean for Curious Mathematicians". Los organizadores de la conferencia dieron a los participantes declaraciones matemáticas relativamente simples para probar en Lean como práctica. Al trabajar con uno de ellos, Morel se dio cuenta de que su demostración requería un lema, un pequeño resultado intermedio, que no se encontraba en mathlib.
“Era una pequeña pieza del álgebra lineal que, por alguna razón, aún no estaba allí. Las personas que llenan Mathlib tratan de comprender todo, pero no se pueden prever todas las opciones ”, dijo Morel, quien ingresó el lema requerido tres líneas en la base.
Otras contribuciones son más significativas. Durante el último año, Gösel ha estado trabajando en la definición de una variedad fluida para mathlib. Las variedades suaves son conjuntos (como líneas, círculos o superficies de una pelota) que juegan un papel fundamental en el estudio de la geometría y la topología. También suelen desempeñar un papel importante en problemas de áreas como la teoría de números y el cálculo. La mayor parte de la investigación matemática es imposible sin ellos.
Sin embargo, las variedades suaves pueden esconderse bajo diferentes formas, todo depende del contexto. Pueden tener un número finito o infinito de dimensiones, tener límites o no tenerlos, estar definidos en varios sistemas numéricos, en el conjunto de real, complejo o p-ádico.números. Definir la diversidad suave es como definir el amor: lo reconoces cuando lo encuentras, pero cualquier definición estricta seguramente dejará caer algunos de los ejemplos más obvios de este fenómeno.
“Al definir las cosas básicas, no es necesario tomar decisiones”, dijo Gösel. "Pero los objetos más complejos se pueden formalizar de 10 a 20 formas diferentes".
Gösel necesita mantener un equilibrio entre especificidad y generalización. “Tenía una regla: quería poder definir 15 usos diferentes de los colectores”, dijo. "Al mismo tiempo, no quería que la definición fuera demasiado general, de lo contrario sería imposible trabajar con ella".
La definición que desarrolló encaja en 1.600 líneas de código, bastante para una definición de mathlib, pero quizás no tanto en comparación con todas las posibilidades matemáticas que abre a Lean.
“Ahora que tenemos el lenguaje que necesitamos, podemos empezar a demostrar teoremas”, dijo.
Encontrar la definición correcta de un objeto con el grado correcto de generalidad es la principal ocupación de los matemáticos que llenan mathlib. Los creadores de la biblioteca esperan definir los objetos de una manera que sea útil hoy en día y, al mismo tiempo, lo suficientemente flexible como para que estos objetos se puedan usar de una manera impredecible hoy.
“Se subraya la necesidad de que todo sea útil para su uso en un futuro lejano”, dijo Macbeth.
Los perfectoides nacen de la práctica
Pero Lean no es solo una herramienta útil, sino que brinda a los matemáticos la oportunidad de volver a participar en su trabajo. Macbeth todavía recuerda la primera vez que probó un programa para ayudar a escribir pruebas. Era 2019 y el programa era Coq (aunque ahora ha cambiado a Lean). Ella no podía parar.
“En un fin de semana loco, trabajé con este programa durante 12 horas seguidas”, dijo. "Fue una verdadera adicción".
Otros matemáticos describen sus experiencias de manera similar. Lean, dicen, es como un juego de computadora, con las mismas hormonas de recompensa que hacen que sea difícil dejar de lado un controlador de juego. "Puede hacerlo durante 14 horas al día sin sentirse cansado y en un estado elevado todo el día", dijo Livingston. "Obtienes comentarios positivos todo el tiempo".
Sebastien Gösel
Sin embargo, la comunidad Lean entiende que para muchos matemáticos, simplemente no hay suficientes niveles en su programa.
"Si cuantificas el porcentaje de matemáticas formalizadas, diría que menos de la milésima parte de un porcentaje está listo todavía", dijo Christian Szegedi, un programador de Google que trabaja en sistemas de inteligencia artificial y que sueña con poder leer y formalizar libros de texto de matemáticas de forma independiente.
Pero los matemáticos están aumentando este porcentaje. Si hoy mathlib contiene la mayor parte del material enseñado por estudiantes de segundo año de la universidad, los participantes del proyecto esperan agregar el resto del programa en unos pocos años, y esto será un logro significativo.
“En los 50 años de estos sistemas, nadie ha propuesto nunca: sentémonos y organicemos una base de conocimiento consistente de matemáticas que describa el material del instituto”, dijo Buzzard. "Estamos creando algo que pueda comprender las preguntas del examen de instituto, esto no ha sucedido antes".
Probablemente pasarán décadas antes de que el contenido de mathlib coincida con la biblioteca de investigación, pero los usuarios Lean están demostrando al menos la posibilidad teórica de crear dicho catálogo, y lograr este objetivo simplemente depende de ingresar todas las matemáticas en la base de datos en forma de código de programa.
Con este fin, el año pasado Buzzard, Masso y Johan Kommelin de la Universidad de Friburgo en Alemania implementaron un proyecto que prueba la viabilidad de este sueño. Aplazaron temporalmente el llenado gradual de la base con material del instituto y pasaron a zonas avanzadas. Su objetivo era identificar una de las mayores innovaciones en matemáticas del siglo XXI: un objeto como el "espacio perfectoido" desarrollado durante los últimos diez años por Peter Scholze de la Universidad de Bonn. En 2018 recibió el Premio Fields por su trabajo, el mayor galardón en matemáticas.
Buzzard, Masso y Commelin querían demostrar que, al menos en principio, Lean puede trabajar con matemáticas en las que los matemáticos están realmente interesados. "Tomaron algo muy complejo y nuevo y demostraron que estos objetos se pueden manipular con un programa para ayudar a escribir pruebas", dijo Mabubi.
Kevin Buzzard
Para definir un espacio perfectoido, tres matemáticos necesitaron combinar más de 3.000 definiciones de objetos matemáticos y 30.000 conexiones entre ellos. Las definiciones se han extendido a lo largo de muchas áreas de las matemáticas, desde el álgebra hasta la topología y la geometría. Ponerlos juntos en una definición fue una poderosa demostración del crecimiento en la complejidad de las matemáticas a lo largo del tiempo, y por qué es tan importante sentar las bases de mathlib correctamente.
“Muchas áreas de las matemáticas avanzadas requieren que conozcas todo tipo de matemáticas que se enseñan a los estudiantes”, dijo Macbeth.
La Trinidad ha logrado definir el espacio perfectoido, pero hasta ahora hay poco que los matemáticos puedan hacer con él. Se requieren muchas más definiciones matemáticas en Lean, hasta que el programa pueda al menos formular esas preguntas difíciles en las que surgen estos espacios perfectos.
"Es bastante tonto que Lean sepa lo que es un espacio perfecto, pero no conoce el análisis complejo", dijo Masso.
Buzzard está de acuerdo con él y califica la formalización del espacio perfectoide como un "truco", un truco que a veces se muestra a las nuevas tecnologías para demostrar su utilidad. Y esta vez el truco funcionó.
"No tienes que pensar que gracias a nuestro trabajo, todos los matemáticos de la Tierra comenzaron a usar programas para ayudar a escribir pruebas", dijo Masso, "pero creo que muchos de ellos notaron esta posibilidad y comenzaron a hacer preguntas".
Pasará mucho tiempo antes de que Lean pueda convertirse en una parte real de la investigación matemática. Sin embargo, esto no significa que hoy el programa sea una imagen de ciencia ficción. Los matemáticos involucrados en su desarrollo comparan su trabajo con la colocación de las primeras vías del tren, el comienzo necesario de una empresa importante, incluso si ellos mismos no pueden viajar por la vía.
"Va a ser algo tan genial que valdrá la pena hoy", dijo Macbeth. "Estoy invirtiendo mi tiempo en ella hoy para que alguien en el futuro pueda tener una experiencia increíble trabajando con ella".