Coq es el futuro de las matemáticas

Las matemáticas funcionan. Esto lo sabemos porque siempre que sumas 1 + 1 el resultado es 2, cuando derivas x2 el resultado es 2x, pero más allá de saber que esto funciona, ¿alguna vez has pensado cómo puedes probar que, no importa qué, todos los números pares son múltiplos de 2? Este tipo de pruebas se denominan pruebas matemáticas y conforman el núcleo de nuestro conocimiento sobre ellas. Siempre que un matemático quiere probar alguna nueva idea que tiene sobre cómo los cuerpos rígidos pueden funcionar en dimensiones superiores, o cualquier otra idea que tenga, debe primero demostrar sistemáticamente, subirlo en un artículo académico para que sus pares lo revisen y con suerte, si no hay errores, ser aceptado como un teorema. Solo hay un problema: las demostraciones son endiabladamente complicadas.

Imagen 1: Una típica prueba matemática

No es solo que para el común de personas, incluso demostrar que los números irracionales tienen infinitas cifras es complicado, es que algunos teoremas son tan complejos que sus pruebas requieren intrincados pasos, asunciones y muchas, muchas páginas. Algunas pruebas modernas pueden tomar decenas o incluso cientos de páginas. Esto entra en contraste con las antiguas pruebas que algunos matemáticos podían hacer brevemente. Algunos matemáticos mencionan que las pruebas se están volviendo tan complejas que verificarlas por completo se ha vuelto una tarea imposible, debido a la profundidad de las mismas y la cantidad de conocimiento requerido para ayudar en su demostración. Pero los humanos no estamos solos, así como los contadores, ingenieros y doctores se han servido de las computadoras para sus demostraciones, también los matemáticos tienen a su disposición los asistentes de pruebas.

¿Qué son los asistentes de pruebas?

Los asistentes de pruebas son programas de computadora que automatizan el proceso de hacer una prueba matemática. Uno de los asistentes de pruebas más populares es Coq, que definen los autores en su sitio web como: "un sistema de manejo de pruebas formales. Provee un lenguaje formal para escribir definiciones matemáticas, algoritmos ejecutables y teoremas junto a un ambiente de desarrollo semi-interactivo de pruebas comprobadas por máquinas" [1]. 

Muchos proyectos hacen uso de Coq, entre ellos CompCert, un compilador para el lenguaje de programación C99 que está escrito y verificado en Coq [2]. Un compilador es un programa que traduce programas en ciertos lenguajes y los traduce en instrucciones que la computadora puede ejecutar nativamente. ¿Qué tiene que ver las demostraciones matemáticas con compiladores? Los programas de computadoras, como todos los otros programas, son propensos a errores y el beneficio de un programa que garantice que va a hacer lo que se le específica que haga es invaluable para entornos críticos como de infraestructura, aviación, medicina, etc. [3].

Imagen 2: Uno de los logos de Coq, palabara que en Francés significa gallo. Tomada de [1]

Otro proyecto que hace empleo de Coq es The Principia Rewrite un proyecto que trata de utilizar las pruebas encontradas en Principia Mathematica y demostrarlas con Coq [4]. Principia Mathematica es sin duda uno de los libros más importantes escritos sobre los fundamentos de la matemática, pero muchas de sus pruebas son bosquejos con pasos faltantes. Un ejemplo de este proceso se muestra en esta imagen:

Imagen 3: Ejemplo de cómo funciona probar un teorema de Principia Mathematica usando Coq. Tomada de [4].

Un poco de polémica

A pesar de la utilidad aparente de los asistentes de pruebas, no fueron recibidos sin críticas. Una de las pruebas más famosas que hizo uso de este tipo de herramientas fue la demostración del teorema de los cuatro colores, el cual dice que "cualquier mapa geográfico con regiones continuas puede ser coloreado con cuatro colores diferentes, de forma que dos regiones adyacentes no queden con el mismo color.

Imagen 4: Mapamundi coloreado utilizando sólo 4 colores, dejando de lado cuerpos de agua. Imagen tomada de [8]

Este teorema fue demostrado en 1989 usando un ordenador para ayudar a reducir el número de posibles configuraciones totales de mapas a 1834, que tenían que ser comprobadas por un computador. La prueba en total tomaba 400 páginas microfilm y fue recibida con emoción, pero también con polémica debido a la dificultad de verificar la demostración (de hecho en su primera publicación se verificó que la prueba tenía un error fatal y se publicó la corrección en 1989) [5].

En 2005, Georges Gonthier subió una prueba empleando Coq. Esta prueba permitió que solo se necesitará confiar en el kernel de Coq para la demostración, en lugar de los programas utilizados en las pruebas anteriores [6].

Imagen 5: Georges Gonthier. Imagen tomada de [7]

Con Coq incluso se pueden hacer motores para blogs que estén formalmente comprobados, o mucho más útil estructuras de datos distribuidas (estas estructuras son sumamente complicadas de hacer correctamente y suelen contener bugs sutiles). Es poco probable que las pruebas formales se cuelen en el día a día de los programadores (Dijsktra intentó y falló), pero las matemáticas y las ciencias de la computación aún encuentran un gran potencial en estas (no tan) nuevas herramientas.

Pensamientos finales

Coq representa un cambio en la manera en como la matemática se está haciendo hoy en día, con el software y las computadoras cada vez tomando un rol más protagónico, pudiendo asistir en pruebas complicadas, con pasos intrincados o donde el número de pasos simplemente es muy grande para que cualquiera pueda tener todos los detalles en su cabeza en un momento dado. Además de esto, Coq tiene la ventaja de ser un lenguaje de programación donde se pueden crear programas que estén formalmente verificados, algo que es sumamente difícil de hacer en la mayoría de los casos cuando se hace uso de herramientas comunes.

Las ciencias de la computación y las matemáticas siempre han estado íntimamente relacionadas, pero nunca tanto como ahora que una computadora puede crear matemáticas.

Referencias

[1] The coq proof assistant. Welcome! | The Coq Proof Assistant. (n.d.). Recuperado 24 de Abril 2022, de https://coq.inria.fr/ 

[2] Compcert.org. 2022. CompCert - Main page. Recuperado 24 April 2022, de https://compcert.org/.

[3] Leroy, X., Blazy, S., Kästner, D., Schommer, B., Pister, M., & Ferdinand, C. (2016, January). CompCert-a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress.

[4] Elkind, L., 2022. The Principia Rewrite. [online] The Principia Rewrite. Recuperado 24 de Abril 2022, de: https://www.principiarewrite.com/.

[5] Mathworld.wolfram.com. 2022. Four-Color Theorem -- from Wolfram MathWorld. Recuperado 24 de Abril del 2022 de https://mathworld.wolfram.com/Four-ColorTheorem.html.

[6] Gonthier, Georges (2008), Formal Proof—The Four-Color Theorem, Notices of the American Mathematical Society, 55 (11): 1382–1393, MR 2463991

[7] "Theorem Proof Gains Acclaim - Microsoft Research". Microsoft Research, 2022, Recuperado 24 de Abril 2022 de: https://www.microsoft.com/en-us/research/blog/theorem-proof-gains-acclaim/.

[8] Contribuidores de Wikipedia, "Four color world map", 2009. Recuperado 24 de abril 2022 de: https://commons.wikimedia.org/wiki/File:Four_color_world_map.svg