Más Allá de Lean: La Diversidad en la Formalización de las Matemáticas

El artículo discute la evolución de la formalización de las matemáticas, destacando la importancia de sistemas como AUTOMATH, Coq, HOL e Isabelle, y cuestionando la popularidad actual de Lean. Se argumenta que, aunque Lean ha facilitado la formalización, no es el único camino y que otros sistemas ofrecen ventajas significativas, como mejor automatización y legibilidad. Se enfatiza la necesidad de no limitarse a un solo enfoque y se menciona el impacto de la inteligencia artificial en la verificación de pruebas matemáticas.