Reseña: Formalising Lie algebras in Lean

Se ha publicado un artículo de razonamiento formalizado en Lean sobre álgebras de Lie titulado Formalising Lie algebras.

Su autor es Oliver Nash (Imperial College in London, U.K.).

Su resumen es

Lie algebras are an important class of algebras which arise throughout mathematics and physics. We report on the formalisation of Lie algebras in Lean’s Mathlib library. Although basic knowledge of Lie theory will benefit the reader, none is assumed; the intention is that the overall themes will be accessible even to readers unfamiliar with Lie theory.

Particular attention is paid to the construction of the classical and exceptional Lie algebras. Thanks to these constructions, it is possible to state the classification theorem for finite-dimensional semisimple Lie algebras over an algebraically closed field of characteristic zero.

In addition to the focus on Lie theory, we also aim to highlight the unity of Mathlib. To this end, we include examples of achievements made possible only by leaning on several branches of the library simultaneously.

El código de las correspondientes teorías se encuentra aquí.

El trabajo se presentará en el Certified Programs and Proofs (CPP) 2022 el 18 de enero de 2022.

Reseña: Why formalize mathematics?

Se ha publicado un artículo sobre razonamiento formalizado titulado Why formalize mathematics?

Su autor es Patrick Massot (del Laboratoire de mathématiques d’Orsay en la Université Paris-Saclay, Orsay, Francia).

Su resumen es

We’ve been doing mathematics for more than two thousand years with remarkable success. Hence it is natural to be puzzled by people investing a lot of time and energy into a very new and weird way of doing mathematics: the formalized way where human beings explain mathematical definitions and proofs to computers. Beyond puzzlement, some people are wary. They think the traditional way may disappear, or maybe even mathematicians may disappear, being replaced by AI agents. These events are extremely unlikely and they are not the goals of the mathematical formalization community. We want to add to our tool set, without losing anything we already have. In this text I’ll explain what we want to add, distinguishing what already partially exists and what is currently science fiction. Examples will use Lean, a proof assistant software developed mostly by Leonardo de Moura at Microsoft Research, but everything I’ll write applies to other proof assistants such as Coq or Isabelle.

El trabajo es una ampliación de la charla con el mismo título impartida el 27 de octubre de 2021 en el seminario New Technologies in Mathematics Seminar Series en Harvard. El vídeo de la charla se encuentra en este enlace.

Finalmente, a continuación se muestra un resumen más detallado de su contenido.

1. Verificar demostraciones

  • La ventaja más evidente de las matemáticas formalizadas es la certeza de que una prueba es correcta cuando ha sido comprobada por un ordenador.
  • La verificación por el ordenador garantiza la integridad y la consistencia a todas las escalas.
    • La consistencia a pequeña escala significa que no hay ningún caso límite olvidado (como el conjunto vacío o el único número primo par).
    • La exhaustividad consiste en asegurarse de que no hay afirmaciones implícitas erróneas.
    • La consistencia a mediana escala significa que no dejan de ser correctos los lemas cuando modificamos definiciones.
    • La consistencia a gran escala significa que no permitimos que se produzcan malentendidos al utilizar un teorema de un documento que tenía una suposición o notación ligeramente diferente.
  • La tecnología actual no permite esperar que pronto tengamos pruebas formales de cualquier artículo publicado porque:
    • La formalización lleva demasiado tiempo por ahora.
    • No tenemos suficiente matemática formalizada sobre la que basarnos.
  • Alternativas posibles:
    • Podemos concentrarnos en partes de teoremas grandes, como en el Liquid tensor experiment.
    • Verificación de pruebas demasiados grandes para el cerebro humano, como en el teorema de los cuatros colores o en la conjetura de Kepler.

2. Explicar y aprender

  • Al escribir textos matemáticos hay que elegir los conocimientos previos asumidos y seleccionar un nivel de detalle.
  • La aplicación más prometedora de las matemáticas formalizadas es el sueño de producir documentos matemáticos que permitan a los lectores elegir dinámicamente el nivel de detalle y el conocimiento usado.
  • Una vez que se entiende una afirmación, se puede pasar a su demostración.
    • La capacidad informática más importante es la visualización del “estado táctico”, que es una lista de todos los objetos y supuestos que son relevantes en ese momento y el objetivo actual de la prueba.
    • Esta información cambia en cada paso de la prueba.
  • La idea es tener un documento progresivo en el que los lectores puedan elegir dinámicamente dónde pedir los detalles cuando los necesiten.
  • Actualmente no tenemos una forma muy agradable de presentar esta información, pero esperamos tenerla en un par de años como máximo.

3. Enseñar

  • Hay que enseñar a concebir y escribir pruebas.
  • Muy a menudo, esto se enseña sólo indirectamente: se pretende que los alumnos aprendan por imitación.
  • Enseñar utilizando un asistente de pruebas tiene el coste obvio de poner una barrera tecnológica a la entrada (aprender sintaxis y navegar por el software). Pero también tiene grandes ventajas.
    • Una ventaja es el estado táctico que se muestra de forma interactiva durante la escritura de pruebas.
    • La obligación establecer formalmente el enunciado y separarlo de la demostración.
  • Ejemplo de demostración en Lean literario:
  • Otra ventaja del uso de los asistentes de pruebas es que los alumnos pueden percibir mucho mejor la alternancia entre las fases en las que la estructura del objetivo dicta el siguiente movimiento y las fases en las que se requiere cierta iniciativa.

4. Crear nuevas matemáticas

  • El ordenador puede
    • Volver a comprobar continuamente todo en cada cambio de definición o enunciado de lema, marcando (casi) instantáneamente lo que hay que modificar.
    • Ayudar a la limpieza, por ejemplo, marcando los supuestos no utilizados.
    • Aclarar qué lemas dependen de otros lemas y definiciones.
    • Demostrar automáticamente pruebas pasos rutinarios o al menos sugerir un paso siguiente.
  • Formalizar mientras se crea es actualmente una enorme ralentización, incluso para los usuarios experimentados. La esperanza es que la tecnología mejore para que la formalización consuma mucho menos tiempo. Aquí puede ayudar alguna forma de inteligencia artificial.
  • Otro sueño que necesita de la IA es un buen motor de búsqueda de enunciados matemáticos.
  • La principal ayuda a la creación puede ser más indirecta. Las matemáticas formalizadas requieren un pensamiento claro.
  • Las matemáticas formalizadas fomentan, o incluso a veces exigen, abstracciones poderosas.

5. Colaborar y divertirse

  • Las matemáticas formalizadas aportan mucha diversión. Parte de esta diversión proviene del aspecto de “videojuego” de los asistentes de pruebas. Pero la verdadera diversión proviene de la colaboración.

Reseña: What is the point of computers? A question for pure mathematicians

Se ha publicado un artículo sobe razonamiento formalizado titulado What is the point of computers? A question for pure mathematicians.

Su autor es Kevin Buzzard (Imperial College in London, U.K.).

Su resumen es

We discuss the idea that computers might soon help pure mathematicians to prove theorems in areas where they have not previously been useful.

El trabajo se presentará en julio de 2022 como una conferencia invitada en el ICM 2022.

Finalmente, se muestra un resumen más detallado de su contenido.

1. Introducción

  • Los ordenadores se han utilizado para ayudar a algunos matemáticos puros a hacer su trabajo desde que existen los ordenadores.
  • Birch y Swinnerton-Dyer utilizaron un ordenador para calcular muchos ejemplos de soluciones de ecuaciones cúbicas en dos variables módulo números primos.
  • Este artículo es un intento de explicar a todos los investigadores en matemáticas puras que los ordenadores pueden utilizarse ahora para ayudarnos no sólo a calcular, sino a razonar.
  • Se trata de la posibilidad de que los ordenadores pronto nos ayuden a demostrar teoremas.
  • No se debe esperar en los próximos 10 años que un ordenador, por sí solo, consiga una demostración de cualquier problema abierto de interés para los matemáticos puros.
  • Lo que se debe esperar en los próximos 10 años:
    • Que los ordenadores ayuden a los matemáticos puros a demostrar teoremas.
    • Bases de datos de matemáticas digitalizadas y con capacidad de búsqueda semántica.
    • Que los ordenadores completen las pruebas de los lemas, señalen contraejemplos a nuestras conjeturas y sugieran resultados que nos podrían ser útiles.
  • La formalización es la matemática reinterpretada como un juego de ordenador.
  • Los primeros asistentes de pruebas por ordenador aparecieron en los años sesenta.
  • Más recientemente han ocurrido dos cosas:
    • Los resultados a nivel de investigación en todas las áreas tradicionales de las matemáticas puras son ahora accesibles a estos sistemas.
    • Muchos asistentes de pruebas modernos admiten “tácticas”, lo que permite a los matemáticos comunicarse con estas máquinas de un modo de alto nivel, similar al modo en que se comunican entre sí.

2. Breve historia de los teoremas verificados formalmente

2.1. El siglo XX

  • Pruebas de
    • La raíz cuadrada de 2 es irracional.
    • Hay infinitos números primos.
    • Si x e y son números reales, entonces (x + y)(x + 2y)(x + 3y) = x³ + 6x²y + 11xy² + 6y³ se puede demostrar con la táctica ring.

2.2. El teorema de los cuatro colores

  • Una de sus formulaciones es la afirmación de que los vértices de todo grafo plano (sin bucles) pueden colorearse con cuatro colores de forma que ningún vértice adyacente comparta un color.
  • En 1976, Appel y Haken lo probaron utilizando un ordenador de manera esencial.
    • En este caso el ordenador se utilizaba para calcular y no para demostrar.
    • La prueba se basa, esencialmente, en un cálculo informático y, por tanto, depende de la corrección del código informático.
  • En 2005, Georges Gonthier verificó formalmente el resultado de Appel-Haken .
    • El trabajo consta de 60.000 líneas de código escritas en el asistente de pruebas Coq.
    • Comprende pruebas en topología y teoría de grafos, al tiempo que verifica formalmente el cálculo informático necesario para terminar la prueba.
    • Gran parte del trabajo consistió en escribir material de base en lugar de formalizar la prueba en sí.

2.3. El teorema de los números primos

  • En 2007, un equipo formado por Jeremy Avigad, Kevin Donnelly, David Gray y Paul Raff verificó formalmente el teorema de los números primos, en el sistema Isabelle/HOL.
    • El trabajo se basaba en las teorías de la aritmética y el análisis real básico.
    • En 2007, las matemáticas más serias de nivel de licenciatura y de máster ya eran, en teoría, accesibles a estos sistemas, al menos en algunas áreas de las matemáticas puras.
  • En 2009, John Harrison formalizó la prueba analítica compleja del teorema de los números primos en HOL Light.
  • En 2016, Mario Carneiro formalizó la prueba en Metamath.
  • Una de las razones por las que el resultado se estaba formalizando de forma independiente en varios demostradores de teoremas era que resultaba extremadamente difícil traducir una demostración escrita en uno de los sistemas a una demostración en otro sistema.
  • En 2020, Mario Carneiro tradujo la prueba a Lean.

2.4. Teorema del orden impar

  • El teorema del orden impar afirma que cualquier grupo finito de orden impar es resoluble.
  • En 2013, un equipo de 15 personas dirigido por Gonthier verificó formalmente una prueba de este teorema en Coq.
  • La prueba es muy larga; un argumento completo (modulo los fundamentos en teoría de grupos y representaciones) se presenta en los dos volúmenes.
  • El teorema está mucho más allá de las matemáticas de nivel de maestría (este trabajo fue una de las razones por las que Thompson fue galardonado con la Medalla Fields en 1970).
  • La prueba de Coq implicó la formalización de los dos libros mencionados anteriormente, además de la teoría de grupos, la teoría de la representación, la teoría de Galois y la teoría de los números.
  • La formalización del material de base ocupó gran parte de los seis años que los autores dedicaron a la prueba.
  • Lo que este trabajo de formalización nos muestra es que los demostradores de teoremas son ahora capaces de operar a este tipo de escala.
  • Por término medio, una línea de matemáticas en los libros de texto correspondía a cinco líneas de código informático, por lo que sabemos que en 2013 el llamado “factor De Bruijn” para este tipo de matemáticas es de alrededor de 5.
  • Los grandes proyectos de formalización como éste son una forma muy eficaz de motivar el desarrollo de bibliotecas de matemáticas fundamentales.
  • Una de las consecuencias de este proyecto de formalización fue que Coq desarrolló una biblioteca muy sólida de álgebra de nivel universitario que, por supuesto, puede utilizarse (y se utiliza) para otros proyectos.

2.5. La conjetura de Kepler

  • La conjetura de Kepler afirma que el empaquetamiento cúbico centrado en la cara es la forma más densa de empaquetar esferas congruentes en el espacio.
  • En 1998, Hales y Ferguson demostraron la conjetura.
    • Parte de la prueba de Hales-Ferguson consistió en la comprobación de más de 23.000 desigualdades no lineales en un ordenador.
    • También se realizaron otros cálculos informáticos.
  • En 2003 Hales anunció un proyecto para verificar formalmente la prueba.
    • El proyecto de formalización tardó unos 12 años en completarse, y comprendió más de medio millón de líneas de código.
    • Uno de los principales beneficios del trabajo es que la biblioteca estándar de HOL Light creció hasta incluir teoremas como el teorema del punto fijo de Brouwer, el teorema de Krein-Milman y el teorema de Stone- Weierstrass.
  • En 2017, Hales dio una charla en la que cuenta la historia de la prueba de Kepler y explica su visión para el futuro de las matemáticas formalizadas.

2.6. Espacios perfectoides

  • Este proyecto implicaba el desarrollo de teorías básicas de localización de anillos y de gavillas en espacios topológicos.
  • El proyecto aclaró que debería ser posible formalizar objetos matemáticos mucho más complejos.
  • A finales de 2017 a Patrick Massot y a Kevin Buzzard se les ocurrió de forma independiente la idea de formalizar los espacios perfectoides. En 2018 Johan Commelin se unió al proyecto.
  • El proyecto se podría resumir como una formalización informática de la única línea matemática “sea X un espacio perfectoide”
  • La principal ganancia fue la ampliación de la biblioteca matemática de Lean, mathlib, con los resultados de la Topología General de Bourbaki así como muchos resultados del álgebra topológica y los inicios de una teoría de campos de valoración discretos.
  • La siguiente pregunta natural es si los sistemas de demostración por ordenador pueden demostrar teoremas complejos sobre objetos complejos.

2.7. Matemáticas condensadas

  • Clausen y Scholze han estado desarrollando una teoría de las matemáticas condensadas, con el objetivo de conseguir que las técnicas del álgebra homológica se apliquen a varios problemas de la teoría de la geometría analítica.
  • Scholze desafió a la comunidad de la formalización para demostrar su Teorema 9.1 en una entrada de su blog.
  • Johan Commelin se convirtió en el líder de facto del proceso de formalización, y Patrick Massot le apoyó y un equipo de teóricos de números algebraicos y geómetras aritméticos comenzó a trabajar en el proyecto.
  • En seis meses, el equipo había crecido hasta contar con más de diez personas y había formalizado una demostración completa del teorema 9.4.
  • En el momento de escribir estas líneas no se ha deemostrado el teorema 9.1, pero es sólo cuestión de tiempo.
  • Esto representa una prueba sustancial de que ahora cualquier matemática pura puede formalizarse con demostradores de teoremas.
  • En muchos proyectos de formalización se suele dedicar una cantidad de tiempo considerable a la formalización del material de base.
  • A medida que las bibliotecas de los demostradores mejoren y empiecen a contener el tipo de material que los matemáticos en activo dan por sentado, habrá menos de estos “costes iniciales”.

2.8. Otros resultados

  • Sebastien Gouëzel formalizó las definiciones básicas de los ∞colectores Ck y C en Lean.
  • Mahboubi y Sibut-Pinote demostraron la irracionalidad de ζ(3) en Coq y Eberl lo demostró en Isabelle/HOL.
  • Han y van Doorn demostraron la independencia de la hipótesis del continuo en Lean.
  • Immler verificó formalmente los cálculos de Tucker utilizados para verificar la existencia del atractor extraño.
  • Mehta y Dillies verificaron formalmente el teorema de Roth sobre las progresiones aritméticas en Lean.
  • Argyraki, Edmonds y Paulson verificaron el teorema de Szemeredi en Isabelle/HOL.
  • La resolución de Ellenberg-Gijswijt de la conjetura del conjunto tope fue verificada en Lean por Dahmen, Hölzl y Lewis.

3. mathlib

  • mathlib:
    • Es la biblioteca de matemáticas de Lean.
    • Es una de las mayores colecciones de matemáticas formalizadas que existen.
    • Actualmente está experimentando un rápido crecimiento.
  • En 2013, Leonardo de Moura inició el desarrollo del Lean Theorem Prover.
  • En 2017, se decidió separar la mayor parte de la parte “matemática” del prover de la parte “central”, y trasladar las matemáticas a una biblioteca propia. De esta forma nació mathlib.
  • En el 2017, mathlib contenía definiciones de grupos, anillos y topología espacios, filtros, una construcción de los números racionales (los naturales y los enteros se quedaron en el núcleo de Lean), y poco más.
  • Johannes Hölzl y Mario Carneiro se convirtieron en los mantenedores de mathlib.
  • La biblioteca es un proyecto gratuito y de código abierto.
  • mathlib tiene ahora más de 200 colaboradores.
  • Uno de los principios de la biblioteca es hacer las cosas “en la generalidad correcta”.
  • La biblioteca no está concebida con fines pedagógicos o de legibilidad; la idea es seguir creando una base sólida para el tipo de matemáticas que se dan en un departamento de matemáticas puras contemporáneo.
  • Es interesante observar que Lean parece estar aprendiendo matemáticas más o menos a la misma velocidad que un estudiante universitario.
  • Para tener una idea actualizada del estado actual de mathlib, lo mejor es echar un vistazo a la descripción completa de mathlib de la comunidad Lean aquí, o a su resumen de las matemáticas de nivel universitario que contiene aquí.

4. Una breve guía de la teoría de tipos

  • Muchos demostradores de teoremas modernos utilizan alguna versión de la teoría de tipos como base.
    • Isabelle/HOL y los otros sistemas HOL utilizan la teoría de tipos simple.
    • Lean y Coq utilizan la teoría de tipos dependiente.
    • Los diversos sistemas HoTT utilizan la teoría de tipos de homotopía.
  • Hoy en día la mayoría de las matemáticas que se realizan en los demostradores de teoremas se hacen en un sistema de teoría de tipos,

4.1. ¿Qué es un tipo?

  • En definiciones como la de grupo, la palabra “conjunto” no significa más que “colección de elementos”.
  • En la teoría de tipos, el papel de “colección de elementos” lo desempeña el tipo.
  • Un tipo es una colección de términos.
  • La definición de un grupo en la teoría de tipos: un grupo es un tipo dotado de multiplicación tal que se cumplen algunos axiomas.
  • La única diferencia es la notación: el a ∈ X de la teoría de conjuntos se sustituye por el a : X de la teoría de tipos.
  • En la teoría de tipos, todo es un término, y todo término tiene un tipo, pero no todo término es un tipo.
  • Una diferencia entre los tipos y los conjuntos es que los tipos no se mezclan: los tipos distintos son disjuntos.

4.2. Tipos inductivos

  • En Lean se pueden definir tipos “inductivamente”. Por ejemplo, la definición de los naturales es así:

    Con la definición se obtienen:

    • constructores_
      • nat.cero ; nat
      • nat.suc : nat -> nat
    • el eliminador del tipo que permite construir funciones cuyo dominio son las naturales y cuyo codominio es otra cosa. En otras palabras, es el principio de recursión.
  • En Lean, la propia igualdad se define como un tipo inductivo

4.3. Las proposiciones son tipos

  • Una proposición es un tipo y sus pruebas son sus términos.
  • La hipótesis h de que P implica Q se convierte en una función h : P → Q.

4.4. Las pruebas son funciones

  • Nueva forma de pensar en la naturaleza de una prueba: se trata de una función que toma como entrada las hipótesis del resultado que se afirma, y devuelve como salida una prueba del resultado.

4.5. Un ejemplo

  • Enunciado:
  • Demostración (se encuentra aquí)

4.6. Fundamentos

  • Los matemáticos suelen tener muy poco interés en los tecnicismos de los fundamentos lógicos de su materia.
  • Las controversias de principios del siglo XX sobre si los métodos no constructivos están permitidos en las demostraciones matemáticas han desaparecido hace tiempo.

5. El futuro

5.1. Un nuevo tipo de documento matemático

  • La formalización ofrece la posibilidad de un nuevo tipo de documento matemático, en el que el lector puede decidir qué cantidad de detalles son visibles.
  • También se podría imaginar que los libros de texto del grado se escribieran de esta manera, en la que las afirmaciones que un estudiante no pueda entender (quizás por ser ambiguas) puedan ser inspeccionadas con más detalle hasta que se resuelvan las dificultades.

5.2. Búsqueda semántica en una base de datos matemática

  • Algo que no va a ocurrir pronto es que todos los matemáticos empiecen a escribir todos sus trabajos en un asistente de pruebas formal.
  • se puede esperar un futuro en el que algunos trabajos se formalicen parcialmente, o incluso completamente, en un demostrador de teoremas.
  • Hales aboga por una versión formalizada de Math Reviews/Zentralblatt. Es decir, un sitio web cuya función sea simplemente exponer formalmente los resultados que se anuncian en las principales revistas de matemáticas.
  • El problema con el plan de Hales es que para poder formalizar los enunciados de los teoremas habría que definir todos los objetos básicos que se utilizan.
  • La comunidad de Lean se ha esforzado por introducir en mathlib algunas de las principales definiciones de la matemática de investigación moderna.
  • Un proyecto relacionado es la formalización de etiquetas en el Proyecto Stacks: una gigantesca base de datos en línea de geometría algebraica, de libre acceso en línea.
  • Formalizar todas las pruebas del Proyecto Stacks no es una idea factible. Sin embargo, formalizar sólo las definiciones y el estado de los teoremas es una tarea absolutamente accesible.

5.3. Comprobación de pruebas

  • Lo que es factible es formalizar partes de la pruebas de grandes teoremas.
  • Los demostradores de teoremas pueden utilizarse para comprobar pruebas que los humanos podrían considerar tediosas.

5.4. La enseñanza

  • Deberíamos enseñar a los estudiantes universitarios a utilizar los asistentes de pruebas.
  • Los demostradores deben ser más fáciles de usar, quizás con interfaces gráficas y documentación más apropiada para los matemáticos.

5.5. Otras ideas

  • Es hora de mirar más allá de cómo solemos enseñar y aprender matemáticas, y tratar de entender cómo nosotros, como comunidad de matemáticos, podemos utilizar la inevitable digitalización del material matemático como una herramienta para mejorar nuestras vidas, y las de nuestros estudiantes.

Reseña: Graph theory in Coq: minors, treewidth, and isomorphisms

Se ha publicado un artículo de razonamiento formalizado en Coq/Ssreflect sobre grafos titulado Graph theory in Coq: minors, treewidth, and isomorphisms.

Sus autores son

  • Christian Doczkal (Université Côte d’Azur, Inria Sopia Antipolis Méditerranée, France) y
  • Damien Pous (Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP, France).

Su resumen es

We present a library for graph theory in Coq/Ssreflect. This library covers various notions on simple graphs, directed graphs, and multigraphs. We use it to formalise several results from the literature: Menger’s theorem, the excluded-minor characterization of treewidth-two graphs, and a correspondence between multigraphs of treewidth at most two and terms of certain algebras.

El trabajo se ha publicado en el Journal of Automated Reasoning

El código de las correspondientes teorías se encuentra aquí.

Reseña: Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi

Sus autores son

Su resumen es

It is nowadays customary to organize libraries of machine checked proofs around hierarchies of algebraic structures. One influential example is the Mathematical Components library on top of which the long and intricate proof of the Odd Order Theorem could be fully formalized. Still, building algebraic hierarchies in a proof assistant such as Coq requires a lot of manual labor and often a deep expertise in the internals of the prover. Moreover, according to our experience, making a hierarchy evolve without causing breakage in client code is equally tricky: even a simple refactoring such as splitting a structure into two simpler ones is hard to get right. In this paper we describe HB, a high level language to build hierarchies of algebraic structures and to make these hierarchies evolve without breaking user code. The key concepts are the ones of factory, builder and abbreviation that let the hierarchy developer describe an actual interface for their library. Behind that interface the developer can provide appropriate code to ensure retro compatibility. We implement the HB language in the hierarchy-builder addon for the Coq system using the Elpi extension language.

El código de HB se encuentra aquí.