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

PorJosé A. Alonso

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.