Matemáticos formalizan más de 260.000 teoremas con el programa Lean

El programa informático Lean ha verificado más de 260.000 teoremas en un proyecto para formalizar todas las matemáticas. Este esfuerzo, financiado con más de 10 millones de dólares, genera debate entre quienes ven una revolución y quienes temen homogeneizar la disciplina.

Un equilibrio histórico entre creatividad y rigor

La búsqueda del rigor tiene una larga historia. El desarrollo del cálculo en el siglo XVII por Newton y Leibniz carecía de formalismo, lo que llevó en el siglo XIX a definiciones precisas de Cauchy y Weierstrass. Esto dio origen al análisis moderno y a la teoría de conjuntos. Sin embargo, algunos físicos como Oliver Heaviside criticaron que este rigor enfriaba el entusiasmo y alejaba las matemáticas de la intuición.

Lecciones del pasado: el caso Bourbaki

En el siglo XX, el grupo Bourbaki priorizó la abstracción y el rigor lógico en sus textos. Su estilo formal tuvo una enorme influencia y moldeó la investigación, pero también margenó campos más visuales como la teoría de grafos durante décadas. Según el historiador Leo Corry, fue un estilo «muy austero». Algunos matemáticos, como Aravind Asok, creen que esta homogeneización disminuyó la diversidad cultural de las matemáticas.

La promesa y el coste de la verificación digital

Lean es un asistente de pruebas que exige que cada paso lógico sea explícito para verificar un teorema. Proponentes como Alex Kontorovich lo ven revolucionario, ya que permite reutilizar partes de pruebas verificadas. Sin embargo, formalizar una prueba en Lean puede llevar desde semanas hasta más de un año. Este gran esfuerzo hace que algunos investigadores, como Asok, cuestionen si el tiempo se emplea mejor en otras actividades, argumentando que las matemáticas tradicionales son «notablemente robustas» pese a los errores.

Nuevos hallazgos y riesgos de homogenización

El uso de Lean ya ha producido nuevos conocimientos. La formalización de una compleja prueba de Peter Scholze en 2021 no solo la confirmó, sino que llevó a una versión más depurada. Kevin Buzzard afirma que el proceso «te obliga a pensar en las matemáticas de la manera correcta». No obstante, existen riesgos. La historiadora Stephanie Dick advierte que, como toda tecnología, Lean podría desplazar la intuición y el enfoque hacia los problemas que el sistema maneja mejor, en detrimento de otros estilos de pensamiento.

Antecedentes: La formalización como motor de cambio

Los intentos por formalizar las matemáticas han reconfigurado repetidamente la disciplina. La respuesta del siglo XIX a los problemas del cálculo no solo rigió ese campo, sino que generó áreas enteramente nuevas como el análisis y sentó las bases de la teoría de conjuntos, demostrando que la búsqueda de rigor puede ser un potente motor de descubrimiento y no solo una comprobación de certeza.

Cierre: Un futuro por definir

El proyecto de formalización con Lean plantea una disyuntiva fundamental entre la verificación absoluta y la diversidad de pensamiento matemático. La historia muestra que los excesos en la formalización, como con Bourbaki, pueden tener consecuencias no deseadas. El futuro de este esfuerzo dependerá de si la comunidad logra equilibrar el potencial de las herramientas digitales con la preservación de la intuición y los múltiples estilos que han enriquecido históricamente a las matemáticas.