Introducción a los asistentes de prueba
quien hizo la transición a la ciencia de datos y trabajo a diario con algoritmos de aprendizaje automático. Estoy fascinado tanto por su aparente magia como por las matemáticas que subyacen en ellas. Abra cualquier biblioteca de aprendizaje automático y encontrará trucos matemáticos que involucran descomposiciones matriciales, convoluciones, curvas gaussianas y más. Éstos, a su vez, se basan en axiomas y reglas aún más fundamentales, como la aplicación de funciones y la lógica.
Durante mi viaje para aprender estos primitivos, coleccioné un estante entero de libros de matemáticas, muchos de los cuales ahora están acumulando polvo. También me matriculé en la Open University, donde asistí a clases a través de Zoom y aprendí sobre sintaxis y axiomas, y luego cómo combinarlos para construir teoremas.
El tema era fascinante: los axiomas son como piezas de juego y movimientos legales en un tablero, mientras que los teoremas son jugadas legales, algunas más interesantes que otras. Probar un teorema significa desenredar el juego lo suficiente para convencer a los jugadores de que es alcanzable, o refutarlo señalando una imposibilidad. Por ejemplo: "Los dos alfiles están en casillas blancas y un alfil nunca puede cambiar a una casilla de diferente color".
Pero a nivel práctico, los cursos eran tediosos. Me dieron archivos PDF para que los resolviera a mano y luego enviara escaneos de mi trabajo en línea. Mientras garabateaba con lápiz sobre papel y luchaba con las tareas del curso, tuve dos ideas:
Construir una prueba es como programar. No hay manera de que pueda involucrarme con las matemáticas en estas condiciones de principios de siglo. Necesito un IDE, con sugerencias de escritura, resaltado de sintaxis y mensajes de error descriptivos, e interactuar con él de forma interactiva.
Mis pensamientos no eran nuevos. La primera idea se llama correspondencia Curry-Howard y se explica a continuación. Este último es el objetivo de los asistentes de prueba como Lean y sus extensiones IDE (normalmente una extensión VS Code).
Asistentes de demostración interactivos versus demostradores automáticos de teoremas
Los verificadores de teoremas como el núcleo de Lean pueden determinar si las expresiones están bien formadas, si los pasos son legales y si la conclusión final es válida. Los asistentes de pruebas interactivos se basan en ellos y también le ayudarán a crear sus pruebas y sugerir pasos. Los demostradores automáticos de teoremas (ATP) intentan encontrar la prueba por sí mismos utilizando técnicas de inteligencia artificial. Lean funciona como verificador de pruebas y asistente, pero combina bien con la IA generativa para funcionar eficazmente como ATP.
Terence Tao transmite pruebas asistidas por IA en su canal de YouTube utilizando Lean 4 y GitHub Copilot. La mayoría de los titulares del tipo "La IA acaba de resolver un problema abierto de x años" probablemente se formalizaron con Lean (ejemplo 1, ejemplo 2 y 3). Proyectos de IA y puntos de referencia como LeanDojo, miniF2F, ProofNet, PutnamBench, FormalMATH, utilizan Lean. OpenAI y Meta han entrenado modelos para usar Lean, y AlphaProof de DeepMind lo usó para ganar una medalla de plata en la Olimpiada Internacional de Matemáticas.
Existe un gran corpus de guías y tutoriales para Lean, así como una buena comunidad, pero el público objetivo no parecen ser desarrolladores con experiencia en otros lenguajes de programación. Estaba luchando por analizar la sintaxis de Lean en mi cabeza y, a medida que aprendí, noté que estaba caminando en territorio sin pavimentar. Esperamos que las siguientes secciones le guíen en este camino.
La correspondencia Curry-Howard
Comencemos con un teorema de lógica simple, algo que quizás tengas que demostrar en una clase de lógica de pregrado:
(P → Q → R) → (P ∧ Q → R)
El operador → denota implicación lógica, pero en la correspondencia Curry-Howard entre pruebas y programas de computadora puede leerse como una función. ∧ es el “y” lógico. En términos sencillos, nos preguntamos si esta afirmación es cierta: "Si tengo una función que, dada P, produce una función de Q a R, entonces si ya tengo P y Q, puedo producir R".
Nota: (P → Q → R) es una “función curry” (Haskell Curry también tiene la culpa), y la sintaxis es equivalente a (P → (Q → R)). En términos de programación, es una función que devuelve otra función, que luego puede invocarse como foo(bar)(baz). Es lógicamente equivalente a que foo reciba tanto bar como baz como una tupla foo((bar, baz)), pero eso es lo que estamos tratando de demostrar aquí. Asimismo, la oración completa podría escribirse como (P → Q → R) → P ∧ Q → R.
Imaginemos esto con un ejemplo concreto: si tengo una máquina expendedora que, dada una moneda (P), devuelve una taza de fideos instantáneos (Q → R), y que, dada el agua caliente (Q), devuelve fideos (R), eso significa que puedo hacer un sistema que, dadas una moneda y agua caliente (P ∧ Q) como entradas, puedo devolver fideos.
Si como programador le pidieran que demostrara que esto es posible, podría verse tentado a hacerlo escribiendo una función que se ajuste a este escenario. En TypeScript podríamos escribir:
Pruébelo en el patio de juegos de TypeScript; modificar cualquier cosa provocará errores de tipografía.
Escrito de forma genérica y simplificada (patio de juegos):
Definimos una función, nuestro teorema, que recibe una función curry (P → Q → R) como parámetro y genera una función que recibe un tipo de producto P ∧ Q y genera R, es decir, (P ∧ Q → R). Esta función actúa como "testigo" de que el teorema lógico es verdadero. La prueba parece sólida e incluso satisface los tipos que deletrean el teorema original en TypeScript:
Digamos esto aún más claramente: la prueba es sólida porque satisfizo el tipo. Las proposiciones son tipos y las pruebas son términos de esos tipos. También vimos que las conjunciones ∧ son tipos de producto/tuplas, y que las implicaciones lógicas Q → R son funciones (q:Q) => R. La flecha es equivalente tanto sintáctica como semánticamente.
Implementemos esto en Lean:
Puedes jugar con él en el patio de recreo de Lean.
El ejemplo es una forma de definir declaraciones anónimas solo para verificar los tipos (a diferencia del teorema de palabras clave), y su tipo (lo que sigue a los dos puntos: hasta la definición :=) es nuestro teorema. La prueba se logra cuando una definición “habita” en este tipo. Como está de moda en la programación funcional, la aplicación de funciones es solo un espacio en blanco: la operación más fundamental se asigna al operador más básico del lenguaje. P ∧ Q es un tipo de producto/tupla, y se accede a sus miembros a través de .left y .right.
Observe que el tipo y la implementación son casi idénticos: el tipo por sí solo es suficiente para determinar el código. De hecho, dada una firma tipográfica, puede usar Loogle para buscar definiciones coincidentes en la biblioteca de Lean.
Otras correspondencias Curry-Howard
* Un mejor tipo de suma sería una unión discriminada: { tag: “left”; valor: P } | {etiqueta: “derecho”; valor: Q }
Lo que aún no has visto
Tipos dependientes
Veamos el siguiente tipo, más complejo:
Significa: "Para todos los valores (∀) de x que son números naturales, 0 es menor o igual a x". lo primero que notamos son los símbolos matemáticos Unicode; estos pueden autocompletarse en el IDE con forall o simplemente sustituirse con la palabra clave ASCII forall.
Esto nos parece que no parece un tipo. El tipo depende del valor de x, algo que normalmente obtenemos de bibliotecas de validación complejas como Zod, no de verificadores de tipos estáticos como TypeScript. Es un tipo que “depende” de valores. Sin embargo, los tipos de Lean no dependen de comprobaciones de tiempo de ejecución como lo hace Zod; sigue siendo un tipo, aunque complejo. Esta es una fuente de confusión al leer la sintaxis de Lean.
Universos
En el patio de juegos o IDE, podemos verificar el tipo de términos con #check:
Ahora verifiquemos el tipo de Nat:
Nat es de tipo Tipo. Pero ¿por qué detenerse ahí?
El tipo es un tipo de Tipo 1, y así sucesivamente. Esto muestra que no existe una distinción sintáctica estricta entre tipos y términos en Lean. Los tipos son términos que tienen sus propios tipos, apilados como capas de cebolla; estas capas se denominan "universos". 3 es un término de tipo Nat y Nat es un término de tipo Tipo, el Tipo n tiene el tipo Tipo (n+1), y así sucesivamente.
Lean debe realizar un seguimiento de los niveles del universo para evitar la paradoja del barbero: “Un barbero afeita a todo aquel que no se afeita a sí mismo, ¿el barbero se afeita a sí mismo?” Con los universos tipo, el barbero es un procedimiento cuyo tipo sólo puede operar sobre elementos de un tipo de un universo debajo de él, no puede operar elementos en su propio nivel, incluido él mismo. Esto evita las paradojas autorreferenciales que podrían causar inconsistencia. La inconsistencia significaría que podríamos demostrar que Falso es verdadero y, a través de ello, probar todas las proposiciones.
Proposiciones
Probemos con un tipo aún más difícil:
En lenguaje sencillo: "¿Es esto cierto? Para cada número natural x, y, z y n, dada una prueba de que n > 2 y x * y * z ≠ 0, podemos producir una prueba de que xⁿ + yⁿ ≠ zⁿ"
Este es el último teorema de Fermat, que dejó estupefactos a los matemáticos durante 358 años después de que Fermat afirmara que su propia prueba no encajaba en los márgenes de la página. La definición utiliza lo siento, que es un marcador de posición para una prueba incompleta. Se compilará pero le dirá: la declaración usa "lo siento". Se siente como usar Any de TypeScript para silenciar sus errores de tipo, pero un revisor podría notarlo y pedirle que corrija el error de pelusa. Proporcionar esta prueba es su "objetivo".
Volvamos a algo más fácil:
Esto es ridículo. ¿Cómo puedo definir un término cuyo tipo es 2 + 2 = 4?
Comencemos mirando el tipo:
El tipo es Prop, abreviatura de proposición. Una proposición es una afirmación que puede ser verdadera o falsa. Como dijimos anteriormente, en la correspondencia Curry-Howard una proposición es un tipo y una prueba es un término o programa de ese tipo. La proposición es verdadera si el tipo tiene “un habitante” y falsa si no lo tiene. Lean no “resuelve” una proposición en un valor booleano verdadero o falso en un sentido computacional; simplemente decimos que es "verdadero" o "falso". Usar Lean como asistente de prueba significa trabajar principalmente con proposiciones.
Detrás de escena, el verificador de tipos de Lean normalizará este tipo en 4 = 4, pero no más. Sólo necesitamos proporcionar un término que habite en este tipo normalizado. Hacemos esto con rfl, un constructor de entidades importado automáticamente desde el paquete Prelude a su espacio de nombres.
Esto funciona. Es una sintaxis declarativa para afirmar que 2 + 2 = 4 es verdadero por reflexividad. Para entender por qué esto funciona, verifiquemos el tipo:
Se trata de genéricos que, por convención, utilizan letras griegas. Las llaves significan que Lean las inferirá por usted.
rfl.{u} es el nombre de la función y su nivel de universo (su capa de los tipos cebolla). {α: Ordenar u} significa que α es un tipo en el nivel del universo u, nada que ver con "clasificable", es solo del tipo "ordenar" u. {a : α} significa que a es un término de tipo α, y el tipo de rfl es en última instancia la proposición a = a. En nuestro caso, α es Nat y a es 4, rfl tiene el tipo 4 = 4, coincidiendo con el tipo Lean normalizado anteriormente. Hemos encontrado un habitante para 2 + 2 = 4 demostrando la proposición por reflexividad.
Táctica
Anteriormente resolvimos nuestro ejemplo de máquina expendedora solo con la aplicación de funciones, pero hay muchas más primitivas interesantes en Lean. En Lean puedes comenzar tu prueba con lo que activa el modo “táctico”:
Esto le permite construir su prueba paso a paso, mientras que el panel derecho de su IDE (InfoView) muestra progresivamente sus suposiciones locales y su objetivo, marcados con ⊢. Las tácticas son una combinación de macros y azúcar sintáctico que resuelven el estado de prueba del núcleo del lenguaje de verificación de tipos. Le ayudan a pensar de forma analítica y declarativa mientras aborda sus objetivos. Es una solución de estilo imperativo dentro de un lenguaje funcional, que se ejecuta dentro de una mónada.
Tendrá que familiarizarse con las tácticas tal como lo hace alguien que aprende SQL con construcciones analíticas como GROUP BY, PIVOT y LEFT JOIN. Al eliminarlo, se mostrará el estado y los objetivos en InfoView:
Tenemos un objetivo que demostrar. Coin y HotWater son propuestas. Noodles es un desconocido del tipo ?u.29, una identificación aleatoria para un nivel de universo aún no asignado. Nuestro objetivo es producir una prueba de (Moneda → Agua Caliente → Fideos) → Moneda ∧ Agua Caliente → Fideos.
Usemos la introducción a la táctica para introducir una suposición en el alcance. Capturará automáticamente el tipo de entrada (Moneda → Agua Caliente → Fideos), una de las pruebas con las que ya “tengo” que trabajar:
InfoView se actualizará y le mostrará los supuestos y el objetivo locales actualizados:
Además de Coin, HotWater y Noodles, ahora tenemos una hipótesis (o suposición) local: noodleVendingMachine, una constante de tipo Coin → HotWater → Noodles (una función de curry). Nuestro objetivo ahora es producir Coin ∧ HotWater → Noodles.
Introduzcamos otra variable que capturará automáticamente la siguiente suposición, de tipo Coin ∧ HotWater:
InfoView ahora muestra:
Ahora solo necesitamos devolver Noodles utilizando nuestra caja de herramientas de tácticas y suposiciones en el ámbito local. Tenemos una función de curry noodleVendingMachine y un tipo de producto (tupla) coinAndHotWater. Apliquemos la moneda y el agua caliente de coinAndHotWater a noodleVendingMachine:
La táctica exacta sirve como palabra clave de retorno cuando tenemos el tipo exacto a devolver. .left y .right son los elementos del tipo de producto/tupla coinAndHotWater, que aplicamos a la función de curry noodleVendingMachine. Recuerde que los espacios en blanco son aplicaciones de funciones.
InfoView muestra:
Esto se puede escribir genéricamente como:
Satisfaciendo nuestro teorema original (P → Q → R) → (P ∧ Q → R) anterior.
Algunas tácticas ayudan a descomponer un objetivo en obligaciones más pequeñas, como introducción, casos, constructor, aplicación o refinamiento. Otros reescriben la expresión utilizando suposiciones de equivalencias, como rw o simp. Otras tácticas normalizan la expresión mediante cálculo o manipulación algebraica, como rfl y ring. Y algunos proporcionan automatización dirigida: linealinto, omega, esopo. Consulta la referencia táctica.
Pensar tácticamente es una habilidad elegante que sólo puede surgir de la experiencia. Para reutilizar un símil anterior, es como un analista de datos que implementa las funciones analíticas correctas y limpia, enriquece y resume tablas sin esfuerzo, o como un ingeniero de software senior que reúne los comandos Bash correctos o reconoce el patrón de diseño más limpio para el trabajo.
Visión general de los demostradores de teoremas
Leibniz soñaba con un lenguaje de pensamiento formal universal (Characteristica universalis) combinado con una calculadora mecánica (Calculus ratiocinator) que pudiera probar todos los teoremas y argumentos filosóficos girando una manivela. Hilbert preguntó: "¿Es esto posible?" — convencido hasta la muerte de que “no hay nada que no sepamos”. Esto se consideraba "el principal problema de la lógica matemática" y "el problema más general de las matemáticas". Gödel reflexionó sobre esto y demostró que algunas verdades no se pueden probar, mientras que Church y Turing demostraron de forma independiente que "a menudo estarás girando esa manivela para siempre", posiblemente iniciando el campo de la informática en el proceso. Para usar la analogía del ajedrez anterior, la demostración automatizada de teoremas es como buscar posiciones ganadoras en el árbol del juego, pero las matemáticas tienen un tablero infinito, por lo que la búsqueda puede no terminar nunca: algunas jugadas son “indecidibles”. Sin embargo, todavía podemos comprobar si una mudanza es legal y aquí es donde nos encontramos con los asistentes de pruebas.
En 1956, Bertrand Russell escribió una carta sobre Logic Theorist, que había demostrado automáticamente teoremas de Principia Mathematica y que a veces se describe como el primer programa de IA:
"Ojalá Whitehead y yo hubiéramos conocido esta posibilidad antes de perder diez años haciéndolo a mano. Estoy bastante dispuesto a creer que todo en la lógica deductiva puede hacerse mediante maquinaria".
Conclusión
Lean tiene una curva de aprendizaje pronunciada, en parte debido a su sintaxis y al uso de tácticas, que debes aprender. Sin embargo, luchar con Lean tiene una recompensa: estás aprendiendo matemáticas. Los tipos, universos, tácticas, teoremas y pruebas no son peculiaridades de otro lenguaje de programación, sino conceptos con los que los matemáticos y lógicos lucharon durante generaciones. No son hechos inútiles para memorizar, sino patrones de pensamiento tan antiguos como Euclides y tan eternos como los teoremas que demostramos.
Una vez que esté familiarizado con los fundamentos, intente pasar a temas más avanzados con Matemáticas en Lean, donde abordará problemas de matemáticas discretas, álgebra lineal, cálculo diferencial y topología. O profundice en los fundamentos comenzando desde cero (literalmente) hasta el libro complementario Lean de Tao del Libro “Análisis I”. Mathlib, la biblioteca colaborativa de Lean, ya tiene 1,6 millones de líneas de matemáticas formalizadas que puede utilizar para conectar todas las ramas de las matemáticas.