El compañero en Lean de Analysis I

• Es un proyecto que traslada los contenidos clave de Analysis I, el libro de análisis real escrito por Terence Tao, al asistente de pruebas Lean
• El proyecto tiene una estructura que encaja muy bien con el objetivo del libro original de enfatizar el rigor, incluyendo la construcción de los sistemas numéricos básicos y la lógica de demostración
• Aprovecha la biblioteca estándar Mathlib, pero también incluye la construcción directa de conceptos clave y ejercicios para que los lectores demuestren por sí mismos
• Se puede practicar completando directamente los espacios en blanco (sorry) en el código de Lean; no se ofrecen soluciones oficiales y es posible ampliarlo mediante un fork
• Es útil tanto para quienes se inician en Lean como para quienes estudian análisis real, ya que ofrece una oportunidad de experimentar el uso real de Mathlib y Lean

---

Descripción general

• Es un proyecto de código abierto que reconfigura "Analysis I", el libro de análisis real de Terence Tao, como una herramienta de asistente de pruebas Lean
• Este libro pone más énfasis que otros textos de análisis en el proceso de construcción de los números naturales, enteros, racionales y reales, así como en las herramientas de teoría de conjuntos y lógica necesarias para ello
• Gran parte del libro se centra en desarrollar una capacidad sistemática de demostración rigurosa, por lo que su estructura encaja bien con un asistente de pruebas como Lean

Características del proyecto complementario en Lean

• Ofrece una “traducción” al formato de Lean de las definiciones, teoremas y ejercicios del libro original
• Estos archivos de Lean incluyen muchos espacios en blanco (sorry) correspondientes a las soluciones de los ejercicios, de modo que el lector puede aprender completándolos por su cuenta
• No se proporcionan explicaciones oficiales ni soluciones, pero el lector puede hacer un fork del repositorio y crear su propia versión con respuestas

Relación con Mathlib y diferencias

• Algunos conceptos ya implementados en Mathlib (la biblioteca matemática estándar de Lean), como los números naturales, se reconstruyen deliberadamente desde cero, y luego también se plantea el proceso de demostrar la isomorfía (equivalencia) con la versión de Mathlib
• Por ejemplo, en Chapter2.Nat se construyen desde cero unos números naturales propios, distintos de los de Mathlib; tras trabajar directamente con los resultados principales, al final se practica en Lean que ambas versiones son equivalentes
• A partir de los capítulos posteriores, se va utilizando cada vez más las definiciones y funcionalidades de Mathlib

Cómo aprender y usarlo

• Este compañero en Lean no solo sirve para estudiar análisis, sino que también funciona como una introducción a cómo formalizar matemáticas en Lean y Mathlib
• Incluye ejercicios estructurados, similares a "Natural number game", para definir y practicar directamente objetos matemáticos dentro del entorno de Lean
• Aunque el código en sí puede compilarse en Lean, no se ha verificado por completo que todos los ejercicios (sorry) sean realmente resolubles, por lo que se necesita playtesting y retroalimentación

Código abierto y contribuciones

• El repositorio es de código abierto y cualquiera puede consultarlo, hacer fork y contribuir
• No se ofrecen soluciones oficiales por separado, lo que permite generar múltiples versiones de resolución
• Al 31 de mayo, el proyecto se trasladó a un repositorio independiente

[GN⁺]

Opiniones en Hacker News

• Me entusiasma mucho esta situación: si este proyecto se mueve a un repositorio independiente, será mucho más fácil compartirlo y encontrarlo. Siempre he sentido curiosidad por las matemáticas, y Analysis de Tao fue el primer libro de texto que me mostró cómo se construyen las matemáticas con rigor de una forma que encajaba con mi manera de pensar como programador. Después también me enganché con Lean, pero sentí que Mathlib era un poco complejo para aprender conceptos matemáticos. Por eso me encanta este proyecto, porque sirve como puente entre el libro y la herramienta.

  • Yo tuve una experiencia parecida. Aprendí sobre convergencia, sucesiones de Cauchy, etc., y recuerdo que este libro fue publicado por una editorial sin fines de lucro en India, Hindustan Book Agency, así que se podía conseguir muy barato.

• Lo que más me emociona de la enseñanza de matemáticas con Lean es la retroalimentación inmediata. Si el estudiante se equivoca en una prueba, no compila. Antes tenía que intervenir una persona, como un TA o un profesor, para dar retroalimentación, pero ahora el compilador de Lean lo informa rápido. Ojalá en el futuro aparezca una función que incluso sugiera correcciones, como hace el compilador de Rust (aunque eso quizá requiera integrar un LLM especializado).

  • También estoy de acuerdo en casi todo, pero creo que el proceso de pensar una demostración también es importante. Mi experiencia con las matemáticas fue hace mucho tiempo, pero recuerdo muchos momentos de "paraíso matemático" en los que me sentaba a pensar despacio escribiendo tareas o problemas en papel. Me preocupa que con Lean eso se convierta más bien en algo de estar tecleando al azar o probando hasta que algo funcione de forma automática. Hace tiempo probé un poco con coq y casi todo el tiempo era solo estarle moviendo cosas. En resumen, los theorem solvers son útiles en muchos sentidos, pero me preocupa que se pierda ese proceso lento de asimilación, conceptualización y surgimiento de nuevas ideas. Me interesa saber qué opinan de eso.

• Comentario sobre que existe un canal personal de YouTube donde se puede ver a Terence Tao usando Lean directamente. No soy experto en el área, pero me pareció fascinante simplemente verlo trabajar, con o sin LLM (https://www.youtube.com/@TerenceTao27)

• Creo que sería realmente interesante comparar y evaluar el enfoque tradicional de "libro de texto" frente al enfoque de Mathlib. Las bibliotecas de matemáticas formalizadas en general tienen la ventaja de expresar los resultados de la forma más general posible, y además es fácil refactorizar la estructura misma de las pruebas para hacerla más elegante. Refactorizar es sencillo porque el sistema siempre rastrea las dependencias lógicas, algo que no es nada fácil cuando solo tienes papel y lápiz. Por eso me parece natural preguntarse si estaría bien enseñar en cursos universitarios una versión de análisis con "máxima generalidad" al estilo Mathlib. Creo que es la misma pregunta para cualquier otra área de matemáticas basada en demostraciones.

  • Al menos en cursos introductorios, no me parece adecuado. Ya hay demasiadas cosas que meter en el plan de estudios: métodos de demostración, programación y teoría básica. La experiencia de profesores que realmente lo han intentado parece ir en la misma línea: para estudiantes avanzados puede estar bien, pero para el estudiante promedio suele ser una pérdida de tiempo.

  • Como matemático que también ha programado durante mucho tiempo, no creo que ninguna formalización programática vaya a desarrollar comprensión fundamental. Mi sesgo viene de que aprendí conceptos a través de artículos. El código a menudo puede ser abrumador en legibilidad porque no siempre cuida el estilo; si ya cuesta leer artículos mal escritos, con código puede ser 10 veces peor porque ni siquiera hay estándares claros, al menos en mi experiencia.

• Me da gusto que la demostración de teoremas vaya ganando atención en áreas matemáticas más mainstream como el análisis. En PLT ya existía un caso representativo: el libro de Winskel, The Formal Semantics of Programming Languages, fue verificado formalmente en Isabelle (http://concrete-semantics.org). Si alguien quiere empezar con theorem proving, creo que ese lado es más fácil y más recomendable. También hay que añadir que los teoremas en análisis ya son bastante difíciles por naturaleza.

  • Tampoco me sorprendería que las pruebas en PL tuvieran una barrera de entrada más baja. A menudo se dice que tienen algo más de rutina: inducción estructural, aplicar inducción, demostrar invariantes, repetir, y así. No he hecho mucho theorem proving, pero nunca he intentado hacer pruebas matemáticas (especialmente de análisis) con un theorem prover. Me pregunto si las pruebas "matemáticas" requieren un enfoque muy distinto, y cuánto se trasladan realmente las habilidades entre ambos mundos. Por cierto, estudié Software Foundations en Rocq (¿tal vez haya un port a Lean?) y me pareció bastante disfrutable.

• Creo que este proyecto y su enfoque encajan muy bien con un tema fundacional como el análisis, pero tengo dos preocupaciones.

  1. Los resultados centrales de análisis en Mathlib se tratan de forma unificada con el concepto de filtros (filter), y en casos especiales por separado con formulaciones tipo epsilon-delta. Supongo que Analysis de Tao usará un enfoque más tradicional de epsilon-delta.
  2. Mathlib es un proyecto que cambia rápido, así que los nombres y la estructura están cambiando constantemente. El problema es que la información de integración tendría que mantenerse de forma continua.
  • Con la indicación de que cada quien puede revisarlo directamente, se comparte también un enlace relacionado porque la mayor parte del capítulo sobre límites de sucesiones está publicada como páginas de muestra: https://link.springer.com/chapter/10.1007/978-981-19-7261-4_6

• Me parece un proyecto muy genial. Analysis I fue el primer libro de matemáticas "de verdad" que yo, siendo ingeniero, realmente pude seguir y estudiar completo de principio a fin. Había intentado varias veces con otros libros (como Rudin) y siempre fracasé. Si existe una versión en Lean, creo que la gente familiarizada tanto con matemáticas como con programación podrá aprender los conceptos con más rigor, y eso me entusiasma.

• Durante años ha habido intentos de hacer una formalización oficial en Lean de Analysis I de Tao, pero siempre ha sido difícil avanzar más allá de unos cuantos capítulos. Durante un tiempo también quise intentar hacerlo yo mismo: pensé que sería útil para quienes estudian el libro publicar pruebas formalizadas junto con el blog de soluciones de Analysis I (https://taoanalysis.wordpress.com/). Ya había compartido material resumido en un Discord privado, pero aquí dejo de una vez varios proyectos y recursos de referencia en Lean que podrían servirle a varias personas (github, gist, documentación oficial, etc.).

  • https://github.com/cruhland/lean4-analysis
  • https://github.com/cruhland/lean4-axiomatic
  • https://github.com/Shaunticlair/tao-analysis-lean-practice
  • https://github.com/vltanh/lean4-analysis-tao
  • https://github.com/gabriel128/analysis_in_lean
  • https://github.com/mk12/analysis-i
  • https://github.com/melembroucarlitos/Tao_Analysis-LEAN
  • https://github.com/leanprover-community/NNG4/ (este no es el libro de Tao, sino la versión Lean4 del juego de números naturales, con contenido casi idéntico al Chapter 2)
  • https://github.com/djvelleman/STG4/ (igualmente, un juego de teoría de conjuntos, parecido al Chapter 3; pero si ves Game/Metadata.lean, hace import Mathlib.Data.Set.Basic, o sea que en vez de definir teoría de conjuntos totalmente desde cero la importa, y en ese caso Lean ya "sabe" toda la teoría de conjuntos, así que quizá no sea perfecto para nuestro propósito)
  • https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c9e7fc (ejemplo de cómo construir enteros)
  • https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/IntegerGame.lean (puede ser el mismo archivo que el de arriba)
  • https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/RationalGameAlgebra.lean (ejemplo de cómo construir racionales)
  • https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality (ejemplo de referencia para definir un tipo Set personalizado)

• Me pregunto qué tan importante sería en la práctica una "prueba de isomorfismo con el objeto correspondiente en Mathlib". Tal vez omitir la parte del isomorfismo no cambie realmente nada sustancial. Por ejemplo, ¿de verdad se usa para cosas como traducir teoremas automáticamente?

  • Este tipo de pruebas de isomorfismo

    1. Te permiten demostrar que el objeto que construiste y el que ya existe en Mathlib son realmente el mismo, sobre todo porque en Mathlib puede estar definido mediante una construcción compleja y muy generalizada, así que eso ayuda a entender la diferencia.
    2. Cumplen un papel decisivo para entender la notación y la terminología oficiales que se usan al leer o escribir sobre ese objeto en Mathlib.

  • Creo que al menos tienen valor pedagógico, en el sentido de que el proceso de convencerse por cuenta propia de que el conjunto y las operaciones que uno construyó son "los mismos" que aparecen en otras partes del libro ya tiene valor en sí mismo.

• Qué bueno que estén apareciendo libros de texto basados en Lean, pero ¿por qué no hay HoTT (Homotopy Type Theory)? También existe un artículo de debate sobre si "Type Theory (HoTT) debería reemplazar a la teoría de conjuntos (ZFC)" (https://news.ycombinator.com/item?id=43196452). También comparten otros recursos comunitarios sobre Lean que salieron esta semana en HN: "100 theorems in Lean" (https://news.ycombinator.com/item?id=44075061) y el proyecto Lean de DeepMind (https://news.ycombinator.com/item?id=44119725)

  • Pero no veo por qué tendría que haber HoTT a la fuerza. Los theorem provers de HoTT todavía tienen poca usabilidad y tampoco hay suficiente documentación. Además, no me queda claro cuál sería exactamente la ventaja de HoTT; normalmente solo parece tener sentido cuando trabajas con estructuras extremadamente peculiares, como en teoría de categorías.

  • Como esto sigue el enfoque de un libro de texto tradicional, la pregunta de "¿por qué no HoTT?" ya viene contestada implícitamente. Además, creo que hay muchos expertos que son escépticos sobre su efecto pedagógico.