El compañero en Lean de Analysis I

 (terrytao.wordpress.com)
2 puntos por GN⁺ 2025-06-01 | 1 comentarios | Compartir por WhatsApp
  • Terence Tao inició un repositorio complementario que traslada definiciones, teoremas y ejercicios del libro de análisis real Analysis I a código Lean
  • Debido a que el libro trata con rigor la construcción de los números naturales, enteros, racionales y reales, además de teoría de conjuntos y lógica, tiene una estructura ideal para aprender con un asistente de pruebas
  • Actualmente cubre parte del capítulo 2, la teoría básica de conjuntos de la sección 3.1 y hasta la sección 4.1 sobre los enteros, e incluye un isomorfismo con los naturales de Mathlib
  • El código compila en Lean, pero todavía quedan muchos sorry, y se recomienda completarlos en un fork en lugar de publicar soluciones oficiales
  • Este material funciona como una ruta alternativa para resolver ejercicios en Lean y, conforme se avanza, también como introducción al uso de Mathlib

Un proyecto para llevar Analysis I a Lean

  • Lean companion to “Analysis I” es un proyecto que “traduce” a Lean varias definiciones, teoremas y ejercicios de Analysis I
  • Los ejercicios del libro también pueden resolverse completando el sorry correspondiente en el código Lean
  • No está previsto alojar soluciones oficiales de los ejercicios en el compañero, y las versiones con los sorry completados pueden hacerse como forks del repositorio

Por qué el libro y Lean encajan bien

  • Analysis I es un texto pensado para complementar los libros tradicionales de análisis real con mayor atención a los temas fundamentales
    • la construcción de los números naturales, enteros, racionales y reales
    • teoría de conjuntos y lógica para desarrollar pruebas con alto nivel de rigor
  • Cuando se escribió el libro, ya existían asistentes de pruebas como Coq y Agda, pero la verificación formal no era una preocupación en ese momento
  • Más adelante, al experimentar con verificación formal, se confirmó que el contenido del libro encaja bien con un asistente de pruebas
  • La teoría de tipos ingenua usada implícitamente en el libro para construir los sistemas numéricos estándar encaja bien con la teoría de tipos dependientes de Lean
  • El soporte de Lean para quotient type también se ajusta a la forma en que el libro hace esas construcciones

Alcance actual de lo ya trasladado a Lean

Relación con Mathlib

  • La formalización está diseñada para separarse de la biblioteca matemática estándar de Lean, Mathlib, en algunos puntos, y depender de ella en otros
  • Mathlib ya incluye una noción estándar de números naturales
  • En esta formalización de Lean, primero se desarrolla Chapter2.Nat reconstruyendo los naturales “a mano”
    • al trabajar dentro del espacio de nombres Chapter2, puede usarse como Nat
    • se establecen resultados básicos en paralelo con los lemas auxiliares sobre naturales que existen en Mathlib
    • muchas de esas pruebas quedan como ejercicios para el lector y por ahora se sustituyen con sorry
  • En la sección epílogo se establece un isomorfismo entre estos naturales alternativos y los naturales de Mathlib
    • más precisamente, ese isomorfismo también está planteado como ejercicio
  • Después de eso, ya no se usa la construcción de naturales del capítulo 2 y se pasa a usar los naturales de Mathlib
  • El plan es mantener en los capítulos posteriores un patrón de dependencia cada vez mayor en definiciones y funciones de Mathlib en lugar de las construcciones propias de los capítulos iniciales

Forma de uso y estado de verificación

  • El código del repositorio compila en Lean
  • Aun así, todavía no se ha probado si todos los sorry del código realmente pueden completarse
  • También hace falta verificar si los lemas auxiliares necesarios o la API de los archivos Lean son suficientes
    • el objetivo es comprobar si los sorry pueden completarse de forma conceptualmente natural, sin depender de técnicas crípticas de programación en Lean
  • Se espera que voluntarios prueben el compañero para confirmar si los ejercicios realmente pueden resolverse en Lean
  • También se agradece cualquier otra retroalimentación

Como material de introducción a Lean y Mathlib

  • Este compañero puede usarse no solo para análisis real, sino también como introducción a Lean y Mathlib
  • En ese sentido, se parece hasta cierto punto a Natural number game
  • Natural number game se superpone bastante en temática con el capítulo 2 de Analysis I

Lecturas relacionadas

1 comentarios

 
GN⁺ 2025-06-01
Opiniones en Hacker News

  • Creo que lo más interesante de enseñar matemáticas con Lean es la retroalimentación inmediata. Si la demostración de un estudiante está mal, simplemente no compila.
    Antes, solo se podía recibir retroalimentación si alguien como un ayudante, un docente o un experto la revisaba, pero ahora el compilador de Lean puede dar retroalimentación rápidamente.
    A futuro sería bueno que el compilador de Lean ofreciera retroalimentación más educativa, como el compilador de Rust cuando sugiere correcciones de código, y quizá haga falta un LLM dedicado.

    • Estoy casi totalmente de acuerdo, pero me preocupa que en el aprendizaje de demostraciones pueda faltar el pensamiento lento.
      Antes, al estudiar matemáticas, uno pasaba mucho tiempo dándole vueltas a una tarea, probando cosas en papel, y ese proceso a veces llevaba a interiorizar conceptos y a tener ideas nuevas.
      Me pregunto si usar Lean no podría convertirse en una forma de probar a lo loco, verificar al azar y volcar cosas. Cuando toqué Coq algunas veces, también me quedó el recuerdo de haber probado principalmente moviendo una cosa y otra.
    • Acorn ya funciona de esa manera. Cuando una demostración falla pero está “casi bien”, muestra sugerencias como estas en VS Code:
      reduce(r.num, r.denom) = reduce(a, b)
      cross_equals(a, b, r.num, r.denom)
      r.denom * a = r.num * b
      No usa LLM; dentro de la extensión de VS Code corre un pequeño modelo local. Ojalá algún día ese pequeño modelo local se vuelva tan potente que supere ampliamente a los humanos. Hay más detalles en https://acornprover.org/docs/tutorial/proving-a-theorem/.

  • Me entusiasma mucho. Ojalá lo muevan a un repositorio separado para que sea más fácil encontrarlo y enviárselo a otras personas.
    Siempre tuve curiosidad por las matemáticas, y Analysis de Tao fue el primer libro que me mostró cómo se construyen las matemáticas de la forma rigurosa que esperaba mi mente de programador.
    Después probé un poco Lean y me resultó igual de satisfactorio, pero Mathlib era bastante complejo para aprender conceptos matemáticos. Por eso me alegra que aparezca un puente entre el libro y la herramienta.

    • Yo también aprendí con ese libro temas como convergencia y sucesiones de Cauchy. Lo publicaba Hindustan Book Agency, una editorial local sin fines de lucro, así que además era muy barato.

  • Da gusto ver que la demostración de teoremas gana impulso en temas matemáticos centrales como el análisis.
    En teoría de lenguajes de programación, cuando las herramientas ya empezaban a pulirse bastante a mediados de la década de 2010, un libro de referencia como The Formal Semantics of Programming Languages, de Winskel, ya había sido verificado formalmente en Isabelle. No es una transcripción 1:1 completa, pero http://concrete-semantics.org es un ejemplo de eso.
    Si te interesa la demostración de teoremas, personalmente creo que esa área es un punto de partida mucho más fácil. Los teoremas de análisis ya son bastante difíciles por sí mismos.

    • No me sorprende que las demostraciones de lenguajes de programación sean más fáciles para empezar. Como dice la gente, parecen tener muchos más procedimientos formalizados.
      Se hace inducción estructural, se aplica la hipótesis inductiva para mostrar que el invariante se mantiene, y se sigue adelante.
      No es que haya hecho muchas demostraciones de teoremas ni demostraciones “matemáticas” como las de análisis con asistentes de demostración, pero si las demostraciones matemáticas requieren un enfoque mucho más distinto, me pregunto cuánta transferencia de habilidades hay entre ambas.
      También quiero mencionar Software Foundations, de Rocq. Quizá haya un port a Lean, pero cuando seguí las primeras partes me pareció bastante cómodo.

  • Sería muy interesante evaluar en qué difiere el enfoque dominante de “libro de texto” del enfoque de Mathlib.
    En general, las bibliotecas de matemática formalizada enuncian los resultados con la mayor generalidad posible y facilitan refactorizar el desarrollo de las demostraciones para que sea más intuitivo y elegante.
    Refactorizar es fácil porque el sistema siempre sigue la pista de qué se deduce lógicamente de qué. Al trabajar con papel y lápiz no se tiene eso, así que muchas veces se pierden oportunidades de rehacer el trabajo.
    También surge naturalmente la pregunta de si tiene sentido enseñar análisis real en pregrado con la versión de “máxima generalidad” al estilo Mathlib. Por supuesto, lo mismo aplica a otras áreas de la matemática basada en demostraciones.

    • Para un curso introductorio, definitivamente creo que no. Ya hay demasiado que aprender: cómo demostrar, cómo programar y además el contenido propio de la materia.
      Tengo entendido que la experiencia de docentes que lo intentaron fue similar. Para estudiantes avanzados puede estar bien, pero para el estudiante promedio es muy probable que termine desperdiciando tiempo de clase.
    • Como matemático que también lleva mucho tiempo programando, creo que cualquier formalismo de tipo programático probablemente no logre inculcar una comprensión de fondo.
      Mi sesgo viene de haber aprendido conceptos matemáticos a partir de artículos.
      Siento que el código añade una carga enorme y que, por lo general, muchas veces no sigue ningún estándar de estilo. Como alguien que ha tenido que leer artículos matemáticos considerados incomprensibles, diría que el código es 10 veces peor porque prácticamente no hay estándares reales de comprensibilidad.

  • En el canal de YouTube del propio Terence Tao también hay algunos videos en los que usa Lean. https://www.youtube.com/@TerenceTao27
    No conozco los detalles, pero fue genial verlo trabajar con y sin LLM.

  • Me parece un proyecto y un enfoque muy buenos para un tema fundamental como el análisis.
    Las preocupaciones que se me ocurren de inmediato son dos. Primero, los resultados centrales de análisis en Mathlib usan el concepto de filtros para tratar los límites de forma general y unificada. Aun así, algunos resultados están especializados en forma épsilon-delta. Supongo que Analysis de Tao usará el enfoque épsilon-delta más tradicional.
    Segundo, Mathlib se mueve rápido y se rompe con frecuencia. Cambian nombres y hay refactorizaciones constantes, así que un repositorio dependiente necesita mantenimiento continuo.

  • Es una idea bastante radical, pero creo que la educación matemática debería enfocarse en crear sistemas de álgebra computacional como Mathematica y demostradores de teoremas como Lean. También debería incluir con fuerza la visualización y las aplicaciones prácticas.
    En el extremo, podría ser una forma en la que no se haga nada de matemáticas en papel y aun así se pueda demostrar dentro de Lean todo lo aprendido.
    Siento que el sistema actual se concentra en cálculos manuales interminables, que parecen demasiado inútiles y aburridos, y hacen que la gente termine odiando las matemáticas.

  • Me encanta que haya un libro de texto de Lean. Pero ¿por qué no hay HoTT?
    “Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?”
    https://news.ycombinator.com/item?id=43196452
    Más recursos de Lean que aparecieron esta semana en HN:
    “100 theorems in Lean”
    https://news.ycombinator.com/item?id=44075061
    “Google-DeepMind/formal-conjectures: collection of formalized conjectures in lean” https://news.ycombinator.com/item?id=44119725

    • La formalización de varias ideas de HoTT está actualmente en marcha dentro de la comunidad de Agda. https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/
      La motivación exacta está fuera de mi campo, así que no la conozco, pero parece que Agda es una mejor manera que Lean para formalizar esas ideas.
      A finales de este año también saldrá un nuevo libro de texto que será una actualización más moderna del libro existente de HoTT, y también tendrá una formalización en Agda.
      https://www.cambridge.org/core/books/introduction-to-homotopy-type-theory/0DD31EC06C80797A50ACE807251E80B6
      https://github.com/HoTT-Intro/Agda
    • HoTT es un tema muy técnico y muy acotado, así que no tiene sentido abordar dos proyectos ambiciosos de este tipo al mismo tiempo.
      HoTT no está ni cerca de ser aceptada como un estándar razonable, y para la mayoría de la gente es un tema en el que se quedan trabados desde el principio.
      Es parecido a preguntarle a un desarrollador de frameworks de JavaScript por qué no hizo un framework para Elm o Haskell.
    • Tampoco sé por qué tendría que haber HoTT.
      Se ha invertido mucho menos trabajo en hacer cómodos de usar los demostradores de teoremas de HoTT, y la documentación también es mucho más pobre.
      Los beneficios de HoTT tampoco están claros. Parece que solo reduce el trabajo cuando se manejan construcciones muy esotéricas de la teoría de categorías.
    • La pregunta “por qué no hay HoTT” es un poco rara.
      Terrence Tao tiene varios libros de análisis, y este es un material complementario en Lean para su primer libro. Él no tiene un libro de teoría de tipos, por eso no hay teoría de tipos de orden superior. Para empezar, lo que se intenta hacer es algo completamente distinto.
    • El solo hecho de que sea material complementario de un libro existente ya responde a “por qué no es HoTT”. Otra razón podría ser que la gente duda de su valor educativo.

  • Muy genial. Analysis I fue el primer libro de matemáticas “reales” que, siendo ingeniero y no matemático, sentí que podía seguir y resolver por completo después de intentar varias veces con otros libros como Rudin.
    Ojalá el material complementario de Lean lo haga más accesible para personas familiarizadas con las matemáticas y la programación que quieran aprender con rigor.

  • Durante los últimos años hubo intentos constantes de formalizar en Lean el libro Analysis I de Tao, y hubo personas que intentaron hacer exactamente lo mismo que Tao está haciendo ahora. Lamentablemente, la mayoría no logró pasar de los primeros capítulos, pero espero que Tao pueda llegar más lejos
    Yo también pensé en intentarlo por mi cuenta. Me parecía que sería útil para quienes siguen el libro agregar pruebas formalizadas de cada ejercicio a mi blog de comentarios sobre Analysis I: https://taoanalysis.wordpress.com/
    También lo publiqué en el servidor privado de Discord del libro, pero como aquí también podría servir, comparto algunos recursos relacionados
    https://github.com/cruhland/lean4-analysis — tomado de 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/ — no sigue el libro de Tao, pero es la versión para Lean4 del juego de números naturales, así que su contenido es muy parecido al del capítulo 2
    https://github.com/djvelleman/STG4/ — es un juego de teoría de conjuntos en Lean4, así que podría parecerse al capítulo 3. Sin embargo, como en https://github.com/djvelleman/STG4/blob/main/Game/Metadata.lean se ve import Mathlib.Data.Set.Basic, parece que importa los conjuntos de Lean en vez de definir conjuntos desde cero y establecer axiomas. Este enfoque podría no ser bueno para el objetivo, porque hace que Lean sepa “demasiado” sobre teoría de conjuntos
    https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c9e7fc — para construir enteros
    https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/IntegerGame.lean — podría ser el mismo archivo que el anterior
    https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/RationalGameAlgebra.lean — para construir racionales
    https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality — muestra una forma de definir un tipo Set personalizado