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.