Formalizando Análisis I en Lean: Un Proyecto de Aprendizaje Interactivo

El autor está formalizando su libro de texto de análisis real de 20 años, "Análisis I", usando el asistente de prueba Lean. Esto no es una simple traducción; implica convertir definiciones, teoremas y ejercicios en código Lean. Los lectores pueden completar los ejercicios rellenando 'sorries' en el código, aprendiendo Lean y la biblioteca Mathlib en el proceso. El proyecto actualmente incluye varias secciones traducidas, haciendo una transición estratégica de la construcción 'manual' de números naturales a la biblioteca estándar Mathlib. El autor invita a voluntarios a probar y mejorar el proyecto.