Este artículo explora la historia y el panorama actual de la formalización matemática, cuestionando la prevalencia de Lean como la única opción viable. El autor, con décadas de experiencia en el campo, argumenta que la reciente popularidad de Lean, a pesar de sus ventajas (una gran biblioteca, comunidad activa y herramientas robustas), ha eclipsado contribuciones anteriores significativas.
El artículo comienza destacando AUTOMATH, un sistema de formalización desarrollado en 1968, que ya incorporaba muchos de los elementos esenciales que se encuentran en Lean hoy en día. Jutting, utilizando AUTOMATH, formalizó los fundamentos del análisis de Landau, un logro impresionante que tardó 20 años en ser igualado. Si bien AUTOMATH tenía limitaciones (notación deficiente y falta de automatización), el autor sugiere que, en algunos aspectos, aún supera a sistemas más modernos como Rocq. También se menciona el trabajo de Boyer y Moore, quienes, aunque inicialmente centrados en la verificación de código (ACL2), formalizaron resultados matemáticos profundos como el teorema de Gödel y el teorema de la reciprocidad cuadrática.
Posteriormente, el artículo revisa el desarrollo de sistemas como LCF, Coq, HOL y Isabelle, destacando cómo el enfoque de LCF, que utiliza un lenguaje de programación funcional (ML) como metalinguaje para el asistente de pruebas, influyó en el desarrollo de estos sistemas. John Harrison, utilizando HOL Light, formalizó el teorema del número primo, entre otros resultados notables.
El auge de Lean se atribuye a la capacidad de Tom Hales para crear una biblioteca de definiciones matemáticas y a la decisión de Kevin Buzzard de utilizar Lean para la enseñanza. Un factor clave en el éxito de Lean fue el abandono de la obsesión por las “pruebas constructivas” que caracterizaba a Coq, una filosofía derivada de la intuicionismo que, según el autor, limitaba su aplicabilidad a la matemática general.
Finalmente, el artículo critica la tendencia a equiparar el concepto de “asistente de pruebas” con el principio de “proposiciones como tipos”, argumentando que esta visión simplifica en exceso la historia del campo y minimiza la importancia de enfoques como LCF, que no se basan en este principio. El autor enfatiza la necesidad de mantener la distinción entre las categorías de tipos y proposiciones, como lo reconoció De Bruijn hace décadas, para evitar problemas técnicos y conceptuales. En resumen, el artículo aboga por una perspectiva más amplia y matizada de la formalización matemática, reconociendo el valor de los sistemas anteriores y evitando el dogmatismo en la elección de herramientas.