La matemática tiene fantasmas

• Lean es un lenguaje de programación diseñado para formalizar matemáticas, y permite que los matemáticos manejen los teoremas matemáticos como si fueran código.
• Los usuarios escriben teoremas, pruebas y axiomas, entre otros, en formato de código, y el proceso de prueba se lleva a cabo mediante un conjunto de comandos llamado tactic.
• Aunque se puede cerrar provisionalmente una prueba con sorry aunque aún no esté terminada, esto es una prueba falsa similar al any de TypeScript.
• Si se agregan axiomas de forma incorrecta (por ejemplo, 2 = 3), surge el riesgo de contradicción lógica y de la posibilidad de probar cualquier enunciado.
• Lean solo obtiene conclusiones sobre los axiomas elegidos y el sistema de pruebas lógicamente válido, por lo que preservar la validez matemática es de gran importancia.

---

Lean: un lenguaje para trabajar la matemática como código

• Lean es un lenguaje de programación especializado en escribir matemáticas formalizadas.
• Los matemáticos usan Lean para expresar la matemática como código y estructurar sus teoremas y demostraciones para poder colaborar y compartirlos.
• Plantea un futuro en el que una gran parte del conocimiento matemático de la humanidad podría volverse código para verificación y composición mecánica.

Primeros pasos en una prueba en Lean

• Es posible declarar un teorema simple en Lean como theorem two_eq_two : 2 = 2 := by sorry.
• Cuando la prueba no está completa, se usa sorry, pero es solo un recurso temporal y no una prueba real.
  • sorry pasa la verificación de pruebas de Lean, pero lógicamente no se puede considerar confiable.
• Para una prueba completa se usan táctica como rfl (reflexividad) para demostrar una igualdad trivial como 2 = 2.
• Lo que ya se ha demostrado puede reutilizarse en otros teoremas con exact, destacando la modularidad.

Axiomas y contradicción: cuando la matemática está embrujada

• Si se agrega un axioma como axiom math_is_haunted : 2 = 3, Lean lo tratará como verdadero.
• Ese axioma puede luego aplicarse en procesos de prueba y permite demostrar conclusiones matemáticamente imposibles (por ejemplo, 2 + 2 = 6).
• Es posible usar la táctica rewrite para sustituir 2 por 3 y terminar el procedimiento de demostración con rfl.
• Si un axioma inadecuado provoca contradicción, en Lean se llega a un estado donde todas las proposiciones son demostrables (colapso lógico).
• En realidad, a principios del siglo XX, paradojas como la de Russell provocaron una revisión profunda de los fundamentos matemáticos debido a contradicciones en sistemas axiomáticos.
• Lean muestra claramente que la elección de los axiomas es decisiva para mantener la validez de un sistema lógico.

Lean como verificador de pruebas (proof checker)

• Si los axiomas se eligen bien y Lean es lógicamente correcto, ofrece conclusiones con fiabilidad teórica.
• Verifica desde igualdades simples hasta teoremas muy complejos (por ejemplo, el Último Teorema de Fermat) siguiendo los mismos principios.
• Un gran teorema se completa como un árbol en el que la estructura total se va armando a partir de la acumulación repetida de pruebas de subestructuras y teoremas.
• Como ejemplo, existe un proyecto a gran escala para formalizar el Último Teorema de Fermat en Lean, y se espera que finalmente se complete un sistema de prueba formal sin pruebas provisionales (sorry).

El placer de aprender Lean

• Hacer pruebas con Lean es una combinación creativa de programación y matemáticas.
• Al principio se trata de aprender a probar proposiciones simples, y luego, gradualmente, el proceso de construir matemáticas cada vez más complejas y profundas con rigurosidad se vuelve una gran fuente de disfrute.
• Los tutoriales oficiales y recursos comunitarios (por ejemplo, Natural Numbers Game, Mathematics in Lean, entre otros) son adecuados para empezar.
• Al usar Lean, al formalizar la lógica por uno mismo, se puede redescubrir la belleza de ideas y argumentos ingeniosos.
• Finalmente se concluye que, con o sin una razón aparente, para cierto tipo de personas Lean brinda una diversión especial.

[GN⁺]

Comentarios en Hacker News

• Últimamente he estado pensando en la idea de reescribir noticias o artículos de no ficción usando sistemas parecidos a Lean (o Lean mismo), tratando cada afirmación como un teorema que debe demostrarse, incluyendo citas dentro de la prueba; por ejemplo, podría manejarse como una prueba compuesta del tipo “si tres fuentes que yo aprobé afirman que esto es cierto, entonces esto es cierto”, y creo que sería posible marcar todo el documento para que se puedan resaltar visualmente las afirmaciones “demostradas”. No sería perfecto, pero sería un intento de resolver otra vez con tecnología ese rigor del que antes se encargaban los medios
  • Formalizar afirmaciones en lenguaje natural es un área llena de dificultades, por razones parecidas a por qué es difícil escribir código que interactúe con el mundo real. Todos los conceptos que damos por sentados (identidad, tiempo, causalidad, etc.) tienen que tratarse con mucho detalle dentro del formalismo para que los hechos puedan conectarse entre sí o siquiera expresarse. Aun así, este problema es realmente fascinante. OpenCog fue un proyecto que llevó esta idea hasta el fondo, y también existe en la academia un campo de investigación aparte llamado representación del conocimiento y razonamiento (KRR). La revista IJCAI también está llena de trabajos relacionados con esto. Y hay muchas lógicas escritas por filósofos para formalizar distintos tipos de argumentación sobre tiempo/modalidad/probabilidad, etc., pero por desgracia no se combinan fácilmente entre sí (salvo que eso se haya resuelto recientemente)
  • Creo que la creencia más importante que deberíamos tener respecto a las noticias no es algo que en su mayoría pueda demostrarse como una colección de afirmaciones absolutas. Me parece que herramientas para calcular cadenas de inferencia, como la probabilidad bayesiana, son más adecuadas. He visto herramientas para hacer estimaciones numéricas de ese tipo
  • Después de tomar matemáticas en la universidad, sentí que mi escritura de no ficción mejoró mucho. Leía ensayos escritos por mi SO (pareja) y por mi hermana menor, y les aplicaba el mismo rigor que a una prueba lógica, tipo “aquí dices que C se sigue de B, pero en realidad falta por qué B se sigue de A, así que no puedes decir que C se sigue de A”. Parece posible convertir esto en un programa con herramientas como los LLM, pero tienen límites claros por las alucinaciones (generar afirmaciones que no están en los hechos)
  • Hay que tener cuidado. Este enfoque podría darle con demasiada facilidad un aura de objetividad lógica a afirmaciones que en esencia son radicales o absurdas. Las posturas políticas de Gottlob Frege, uno de los padres de la lógica moderna, podrían servir como advertencia enlace relacionado
  • Me parecería más interesante una forma de dibujar como un mapa la estructura argumentativa completa de un tema específico. Por ejemplo, partir de una gran pregunta como “¿Dios existe?”, y desplegar de forma jerárquica todos los argumentos a favor y en contra, las objeciones a esos argumentos y las contraobjeciones. Para cada afirmación, citas del tipo “Platón hizo este argumento” servirían no tanto como evidencia, sino para dar contexto histórico. Lo clave no sería decidir quién gana, sino construir un mapa argumentativo para no seguir dando vueltas sobre los mismos puntos
• Me pregunto si lo que estamos construyendo al final es una especie de diccionario de pruebas que parte de unas cuantas verdades autoevidentes, y sobre ese diccionario se van apilando lógicamente todo tipo de pruebas. Entonces las pruebas nuevas serían solo combinaciones lógicas de pruebas ya existentes. ¡Ojalá hicieran de esto un juego estilo Zachtronics! Un juego llamado Euclidea me da esa sensación en el área de la trigonometría, y la idea de ir apilando así una torre de lógica me parece súper atractiva. Me pregunto si las matemáticas puras son justamente eso, si los profesores de matemáticas puras sienten placer al expandir ese diccionario lógico, y recuerdo que había un matemático famoso que hizo una lista de pruebas básicas; si alguien sabe quién (o qué) era y cómo se llama, estaría genial. Supongo que probablemente sean los axiomas
  • Ya existe un juego relacionado, aunque quizá no sea exactamente lo que quieres (y no es un juego sobre construir todas las matemáticas). Lo jugué y fue bastante divertido. El leanprover-community/nng4 mencionado en este artículo es justo un ejemplo de eso
  • Respondiendo a “quiero que conviertan esto en un juego estilo Zachtronics”: podría decirse que las matemáticas son justamente ese juego (medio en broma), aunque creo que una versión como juego también sería realmente divertida. Las matemáticas puras sí son justo ese sistema. En licenciatura sí se siente así, aunque ya al subir a investigación en artículos cambia un poco. Si buscas esa sensación de juego, también recomendaría revisar un libro de álgebra abstracta como Dummit and Foote; demostrar cosas tiene una diversión de tipo lúdico. Y si te atoras, los libros famosos suelen tener explicaciones en línea
  • Puede que te refieras a los axiomas de Euclides, que son un sistema donde se definen conceptos como punto, línea, plano y líneas paralelas. Ese sistema se rompe sobre una esfera en vez de un plano. O quizá te refieras a la teoría de conjuntos de Zermelo-Fraenkel (ZF/ZFC), sobre la que se construye toda la matemática moderna
  • También hay un juego llamado Bombe, una variante de Buscaminas. En vez de abrir celdas directamente, juegas creando reglas de “cuándo se puede poner una bandera”. A medida que sube el nivel, las reglas se van encadenando como si fueran lemas. Y cuando mejora la habilidad del jugador, también puede relajar las restricciones del conjunto de herramientas para generalizar enlace del juego
  • Las matemáticas son esencialmente el proceso de partir de axiomas y derivar conclusiones. Claro, quizá no sea solo eso, pero a mi nivel así lo entiendo por ahora
• Es medio quisquilloso de mi parte, pero me parece raro decir que el teorema two_eq_two se ve como una función. Como no tiene argumentos, en realidad se parece más a una constante (aunque sí, ya sé que una constante también es una función sin argumentos). Creo que sería más convincente usar x_eq_x abajo y aplicarlo como función en 2_eq_2

  theorem x_eq_x (x:nat) : x = x := by
    rfl
  
  theorem 2_eq_2 : 2 = 2 := by
    exact (x_eq_x 2)
  

  Aquí x_eq_x sí parece una función, y en 2_eq_2 de hecho se usa así
  • ¡Es una observación correcta! No lo hice así porque la forma en que Lean maneja argumentos (sobre todo conceptos como dependent types — dar x y recibir como resultado una prueba de x = x) todavía me resulta algo ajena, y es un tema que quiero tratar por separado. Planeo hablar de eso en el siguiente artículo
• La dificultad que sentí al aprender Lean es que las tactics (rfl, por ejemplo) son demasiado amplias, y ni siquiera con tutoriales es fácil captar su significado exacto. Por ejemplo, en C puedes rastrear cambios de estado hasta el nivel de bits, pero Lean se siente medio difuso. Y la sintaxis de la táctica rewrite (rw) también me parece poco natural
  • En Coq (ahora Rocq) también me costó siempre adaptarme a las tactics. Por ejemplo, tuve experiencias donde tenía “A = B” y “P(A,A)” e intentaba pasar a “P(A,B)”, pero rewrite no funcionaba por razones difíciles de explicar (supongo que por un tema con definiciones de estructuras intermedias). En cambio, Metamath y la base de datos set.mm hacen que pruebes todo sin tactics, solo con inferencia concreta (usando reglas como ax-mp), aunque eso tampoco es fácil porque entonces tienes que memorizar un montón de lemas utilitarios
  • Esa es una de las razones por las que prefiero Agda. Agda prácticamente no tiene tactics, y usando la correspondencia Curry-Howard escribes directamente los términos de prueba como si fuera un lenguaje de programación funcional. A cambio, si eres perezoso para abstraer y crear funciones, hasta lo trivial se vuelve absurdamente tedioso, así que hace falta disciplina
  • Al menos en Lean existe la ventaja de que puedes ir haciendo "go to definition" en las tactics para ver cómo funcionan internamente. Cuando estás aprendiendo, la cantidad de cosas abruma, pero al final sí puedes inspeccionarlo todo (aunque cuando llegas a teoría de tipos básica ya cuesta seguirle la pista). Y sobre que la sintaxis de rewrite no te parece natural, me da curiosidad: ¿qué forma de rewrite te parecería natural?
  • Algo que me pareció interesante es que todas las tactics están en código de “nivel de usuario”, fuera del kernel de pruebas. Tiene sentido, porque quieres mantener pequeño y estable el kernel verificado. Pero eso también significa que si las tactics cambian con una actualización o una corrección, podrían romper pruebas existentes. Me pregunto hasta qué punto eso es un problema en la práctica
  • Contra lo que esperaba, pensé que en Lean reflection y rewrite serían más fundamentales que la suma. Lean trae suma incorporada, pero parece que tienes que escribir rfl o rewrite cada vez. Supongo que quizá exista alguna versión con algo tipo prelude que automatice eso
• Me pregunto si en Lean hay alguna forma de leer proofs de manera no interactiva, porque al jugar el natural number game me costaba muchísimo leer pruebas que solo eran una lista de comandos rw [x]. En el editor puedes ver el estado de cada línea, pero hay que estar haciendo clic todo el tiempo y se rompe el flujo. Si en Python no hubiera sangría y hubiera que hacer clic para entender el flujo mirando solo la estructura de bloques, sería parecido. Puede que desde mi perspectiva eso se deba a que al inicio del juego las órdenes están muy limitadas, pero me pregunto si en un entorno completo de Lean ese flujo mejora

  • ¿Hay alguna forma de leer pruebas en Lean de manera no interactiva?
    Yo también me lo pregunté hace poco y estuve buscando. El blog lean-in-latex ofrece una forma de seguir ese flujo fuera del editor y sin hacer clic, y además puedes ver cómo lo aborda la comunidad de Lean

  • Rocq antes tenía algo llamado “lenguaje de prueba matemático”. Cuesta encontrar ejemplos reales de uso, pero era algo así

    Lemma foo:
      forall b: bool, b = true -> (if b then 0 else 1) = 0.
    proof.
      let b : bool.
      per cases on b.
        suppose it is true. thus thesis.
        suppose it is false. thus thesis.
      end cases.
    end proof.
    Qed.
    

    Este enfoque hacía que se leyera más como una “prueba escrita a mano” de un artículo, pero casi nadie lo usó y desapareció. El lenguaje de pruebas Isar de Isabelle es parecido y, de hecho, está más cerca del enfoque estándar. Ejemplo:

    lemma "map f xs = map f ys ==> length xs = length ys"
    proof (induct ys arbitrary: xs)
      case Nil thus ?case by simp
    next
      case (Cons y ys) note Asm = Cons
      show ?case
      proof (cases xs)
        case Nil
        hence False using Asm(2) by simp
        thus ?thesis ..
      next
        case (Cons x xs’)
        with Asm(2) have "map f xs’ = map f ys" by simp
        from Asm(1)[OF this] ‘xs = x#xs’‘ show ?thesis by simp
      qed
    qed
    

    Ahí se deja clara toda la estructura lógica y los resultados intermedios, y solo donde importan los detalles se abrevia con by ... usando una tactic. No sé si Lean tiene algo así, pero al menos podría servirte como palabra clave de búsqueda o como tema para preguntar en el foro de Lean
  • ¡Muy buena pregunta! Todavía soy principiante, así que no diría que mi opinión sea completamente confiable, pero comparto lo que siento. Tras usar Lean un par de meses, leer código de pruebas no se siente igual que leer código de programación; se parece más a “escanearlo”. Tiendes a fijarte en la estructura general del argumento, en qué tactic se usa y en qué lemas aparecen. El estilo real del código Lean usa sangría cada vez que aparece un nuevo goal, y al cerrar un goal se vuelve a desindentar. Así que la forma del argumento (“shape”) importa mucho para leerlo. Mira este ejemplo de mi PR. Cuando te acostumbras a las tactics, ya reconoces que intro significa entrar a un cuantificador, que constructor significa dividir el goal, etc. Al final, las tactics son una especie de macro/DSL que construye un árbol de prueba (term tree). Cuando veo código de prueba, lo siento como manipulación de árboles (dividir piezas, llenar huecos en orden, etc.). Aun así, sigue siendo cierto que para saber exactamente qué afirma una assertion a mitad del código todavía tienes que hacer clic. Las pruebas con buenas ideas se pueden leer con claridad, como la progresión lógica de un artículo. Por eso, quien quiere transmitir intención termina escribiendo con nombres legibles, una progresión clara, extrayendo lemas pequeños y poniendo primero las hipótesis para resolver luego con pruebas cortas. En cambio, las partes que mecánicamente son fastidiosas pero que a ojos del matemático son obvias suelen resolverse con “golfing” (hacerlo lo más corto posible). Ese estilo golf a menudo acorta el código, pero solo toca las partes que el humano capta intuitivamente. En resumen: en Lean la estructura de lectura es implícita, aunque hay maneras de hacerla más clara, y mientras más dominas las tactics, mejor captas la estructura sin necesidad de hacer clic. A veces basta con recorrer los nombres de los lemas para entender el flujo general, y el orden puede reconstruirse con facilidad
• Me gustó muchísimo el contenido. Creo que muy poca gente puede explicar esto de una manera tan fácil de digerir. El truco es mostrar todos esos pasos pequeños que los expertos normalmente se saltan
  • ¡Gracias!
• Me pregunto si en este hilo alguien podría dar su opinión sobre el futuro de Lean frente a idris/coq/agda. Quiero estudiar representación del conocimiento, pero antes de meterme a fondo en cualquiera me preocupa el tamaño de la comunidad y el riesgo a futuro. Ya antes invertí tiempo en clojure core.logic y me quemé por el poco interés y la comunidad pequeña, así que ahora me cuesta empezar con facilidad
  • Por experiencia real, siento que Lean y Coq/Rocq se usan muchísimo más que Idris y Agda, y también tienen bibliotecas y comunidades más grandes. Rocq se usa sobre todo mucho en verificación de programas, pero creo que eso se debe a que tiene más historia y varias rarezas; Lean podría alcanzarlo pronto. Lean es el más común para probar teoremas matemáticos. Entre los proyectos famosos de Rocq están CompCert, CertiCoq y sel4, y también hay casos de verificación de software real para aviación (puedes ver una lista de proyectos). En Lean hay grandes proyectos como mathlib (colección de pruebas matemáticas), el último teorema de Fermat (proyecto de demostración de FLT), PFR, etc. Según entiendo, Idris y Agda no tienen muchos proyectos del “mundo real”, aunque podría estar equivocado. De cualquier forma, todas estas comunidades son muy pequeñas comparadas con lenguajes o ecosistemas como C++ o JavaScript. Y además, la verificación de programas en la práctica es un trabajo muy lento y aburrido. Quizá algún día haya un cambio de fondo con el avance de la IA, pero aun así las habilidades que aprendas seguirán sirviendo
  • En realidad, no creo que tenga mucho sentido “apostarle” a este campo. A la mayoría de los matemáticos no les interesa demasiado la formalización, porque la brecha entre las pruebas escritas a mano y la sintaxis rigurosa que exige la computadora es grande. Lo mejor es acercarse a esto por diversión, por aprender y practicar. En cuanto al futuro, Lean es probablemente el más activo últimamente, pero cada uno tiene una base de usuarios vieja detrás, así que es difícil sacar conclusiones definitivas
• Me pregunto si, sin ninguna técnica ni truco especial, simplemente lanzándole cosas aleatorias a Lean y viendo si Lean las acepta, podrían aparecer descubrimientos interesantes; o si sería posible automatizar eso con sistemas automáticos o llm para probar todo tipo de pruebas/teorías difíciles y ver si funcionan o no. La pregunta quizá suene rara, pero apenas entiendo Prolog
  • Como alguien que trabaja profesionalmente en programación certificada, diría que la IA generativa y los métodos formales son una combinación ideal. De hecho, creo que si los LLM van a reemplazar a los programadores dependerá de qué tan bien logren combinar programación certificada con razonamiento combinatorio.

    ¿Aparecen hallazgos interesantes si lanzas cosas al azar?
    La IA tradicional funciona bien en problemas con pocos estados posibles, como damas. Ajedrez ya es más difícil, y go es tan complejo que con IA no tradicional era prácticamente imposible sin aprendizaje automático. Los lenguajes formales tienen un número de casos y estados explorables absurdamente grande. Cuando la naturaleza del problema está bien delimitada, un SMT solver puede hacer fuerza bruta. SMT solvers y proof assistants originalmente eran ramas distintas de los métodos formales, pero hoy se complementan cada vez más (véase Sledgehammer, Lean-SMT)
    ¿Y si hacemos que un llm o sistema automático pruebe teorías o pruebas arbitrarias?
    Eso todavía no es investigación completamente mainstream, pero sí se ha intentado bastante. Incluso antes del boom de los LLM hubo financiamiento grande durante años. Están intentos antiguos como “Learning to Find Proofs and Theorems by Learning to Refine Search Strategies”, y trabajos recientes como DeepSeek-Prover. Todavía está totalmente abierto cómo entrenar estos sistemas y hasta dónde podría llegar su potencial futuro.
    Hoy por hoy, los LLM todavía flojean bastante con los lenguajes de Rocq y Lean, y cuando dan una respuesta incorrecta corregirla puede ser muy doloroso. Aun así, espero que con el tiempo el nivel de las herramientas de IA suba mucho

  • ¡Este es de verdad un campo de investigación y experimentación muy activo!
    La comunidad de Lean se reúne mucho en Zulip, y en el canal Machine-Learning-for-Theorem-Proving puedes revisar varios hilos de referencia
• Yo empecé a interesarme por Lean por alphaproof, y esta introducción me gustó muchísimo. ¿Podrías contar qué estás haciendo tú en Lean?
  • Por ahora solo estoy estudiando matemáticas con Lean. En concreto, estoy siguiendo el texto de Lean de Tao y voy llenando por mi cuenta las partes de sorry que dejaron vacías en los ejercicios (mis soluciones están aquí)
• Me pregunto si Lean tiene algún modo de verificación que impida automáticamente el uso de cosas no confiables (proof con sorry) o la introducción continua de axiomas adicionales. Por ejemplo, ¿se puede comprobar que “esta proof no usa sorry de ninguna manera” y que “depende solo del poder demostrativo de un conjunto fijo de axiomas”?
  • Creo que el #print axioms some_theorem mencionado al final del artículo podría ser justo el ejemplo que buscas. Con eso puedes ver si la prueba depende directa o indirectamente de sorry o de axiomas no revisados
  • Puedes usar print axioms para verificar que no se hayan agregado axiomas extra. Y también puedes fijarte en si compila sin warnings ni errores. La utilidad SafeVerify también detecta algunos trucos que encontraron sistemas de RL
  • Aquí hay información de que esto también se puede hacer con macros