Qué es Lean y Mathlib: demostraciones que se comprueban solas

Existe un corrector que revisa cada paso de una demostración, no se cansa, no se fía de la intuición y no admite un «esto es evidente». Si hay un hueco, por pequeño que sea, te dice dónde. Se llama Lean y es de código abierto. Alrededor de él ha crecido una biblioteca comunitaria de matemáticas, Mathlib.

Qué es una demostración formal

Una demostración en papel es un texto para convencer a otra persona. Funciona, pero depende de que el lector entienda lo sobreentendido. Una demostración formal es otra cosa: está escrita en un lenguaje tan preciso que un programa puede comprobar, regla por regla, que cada paso se sigue de los anteriores. A los programas que hacen esto se les llama asistentes de pruebas.

Lean se presenta a sí mismo como un lenguaje de programación y asistente de pruebas de código abierto, con un núcleo de confianza mínimo. Esa última expresión es la clave. Una prueba puede construirse con automatismos muy sofisticados, pero al final pasa por un núcleo pequeño que la revisa. La confianza de la prueba se concentra en ese núcleo, no en cada táctica.

Quién hay detrás

Lean lo creó Leonardo de Moura en 2013. Tao y Scholze aparecen en esta historia como protagonistas de dos grandes proyectos, no como creadores de Lean. Lean 4, la versión actual, es una reescritura completa escrita en el propio Lean; De Moura y Sebastian Ullrich la describieron en un artículo presentado en la Conference on Automated Deduction en julio de 2021.

En julio de 2023 los dos fundaron el Lean FRO, una organización sin ánimo de lucro que depende de Convergent Research. Su misión declarada es avanzar los sistemas críticos de Lean, ampliar su influencia y orientarlo hacia la autosostenibilidad a largo plazo. Entre sus apoyos figuran Gerko (XTX Markets), Sloan, Simons, Convergent Research, Harmonic y Amazon. El 24 de julio de 2025 se anunció una donación de 10 millones de dólares de Gerko, repartida a partes iguales: 5 para el Lean FRO y 5 para Mathlib.

Y Mathlib no es Lean. Lean es el lenguaje; Mathlib es una biblioteca de matemáticas escrita en ese lenguaje por una comunidad abierta, con la idea de reunir las matemáticas en un único edificio coherente. Ambos son software libre. La comunidad publicó una descripción técnica en arXiv el 21 de octubre de 2019. Según la página oficial de estadísticas, consultada el 15 de octubre de 2026, Mathlib tenía 138 028 definiciones, 290 462 teoremas y 772 contribuidores. Son cifras de un día concreto: la página no lleva fecha y los números cambian continuamente.

Un teorema pequeño, de verdad

Veamos Lean trabajando. Este código compila con Lean 4.35.0, la versión publicada el 12 de octubre de 2026:

theorem dos_mas_dos : 2 + 2 = 4 := by decide

theorem suma_conmutativa (a b : Nat) : a + b = b + a := by
  omega

theorem cero_mas (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [Nat.add_succ, ih]

El primero es casi un chiste: decide le pide a Lean que calcule y compruebe. El segundo afirma que $a + b = b + a$ para cualesquiera naturales; la táctica omega sabe resolver este tipo de aritmética lineal.

El tercero es el interesante, y conviene leerlo despacio. Parece obvio que $0 + n = n$, pero Lean define la suma de naturales recorriendo el segundo sumando: $n + 0 = n$ y $n + (k+1) = (n + k) + 1$. Con esa definición, $n + 0 = n$ sale directamente de la primera regla. En cambio $0 + n = n$ no sale de ninguna: hay que probarlo, y la herramienta es la inducción.

El razonamiento tiene dos piezas. El caso base es $0 + 0 = 0$, que se cumple por definición (rfl, «reflexividad»: ambos lados son lo mismo). El paso inductivo supone que $0 + k = k$ (la hipótesis de inducción, ih) y debe probar $0 + (k+1) = k+1$. Por la segunda regla de la suma, $0 + (k+1) = (0 + k) + 1$, y por la hipótesis eso es $k + 1$. Es exactamente lo que hace la línea rw [Nat.add_succ, ih]: reescribe con la regla y luego con la hipótesis. Como un dominó: la primera ficha cae, y cada una derriba a la siguiente.

Lean permite preguntar de qué se fía una prueba. Con la orden #print axioms cero_mas responde que este teorema no depende de ningún axioma. Con Mathlib cargada, una línea basta para algo más ambicioso: theorem raiz_dos_irracional : Irrational (Real.sqrt 2) := irrational_sqrt_two también compila. La demostración ya estaba en la biblioteca, y esa es la gracia: cada resultado formalizado es un ladrillo disponible para el siguiente.

Dos historias grandes

El reto de Scholze. El 5 de diciembre de 2020, Scholze propuso en el blog del proyecto Xena el llamado Liquid Tensor Experiment. Se trataba de formalizar el teorema principal sobre espacios vectoriales «líquidos» de Clausen y Scholze. Escribió que había pasado buena parte de 2019 obsesionado con la prueba, «casi volviéndome loco» (en sus palabras, almost getting crazy over it), que creía que podía ser «mi teorema más importante hasta la fecha» (my most important theorem to date) y que le quedaban «pequeñas dudas» (some small lingering doubts).

El proyecto lo lideró Johan Commelin con el apoyo de Scholze, y se completó el 14 de julio de 2022, año y medio después del reto. Lean no «descubrió» nada: comprobó que la demostración se sostenía.

La conjetura PFR. En noviembre de 2023, Timothy Gowers, Ben Green, Freddie Manners y Terence Tao subieron a arXiv una demostración de la conjetura de Marton (también llamada PFR) en característica 2. Su enunciado dice, en el lenguaje de los conjuntos de vectores con coordenadas 0 y 1 (el espacio $\mathbb{F}_2^n$): si un conjunto $A$ cumple $|A+A| \le K|A|$, es decir, si al sumar sus elementos entre sí apenas se genera más conjunto, entonces $A$ se puede cubrir con a lo sumo $2K^{12}$ clases de un subespacio $H$ con $|H| \le |A|$.

Un caso límite ayuda a ver el sentido. Si $A$ ya es un subespacio, entonces $A + A = A$, o sea $K = 1$, y la conclusión se cumple con una sola clase del propio $A$. La conjetura dice que una «casi estructura» aritmética implica un «casi subespacio», con constantes que no dependen de $n$. La demostración se apoya en desigualdades de entropía de Shannon.

Pocos días después, a mediados de noviembre, Tao lanzó el proyecto de formalización en Lean 4 junto con Yael Dillies y Bhavik Mehta, apoyándose en Blueprint, una herramienta de Patrick Massot: un plan en LaTeX legible por humanos, enlazado con el código y con un grafo de dependencias que se va poniendo en verde a medida que se formalizan los pasos. Se anunció completada el 5 de diciembre, menos de un mes después del artículo. La prueba matemática es de los cuatro autores y Tao dirigió la formalización. Tanto el artículo de 2023 como su formalización tratan la característica 2; los mismos autores extendieron después el resultado a los grupos abelianos de torsión acotada. Además, Jyun-Jie Liao rebajó el exponente: la formalización incorporó una versión de su argumento con exponente 11, y su artículo de abril de 2024 llega a 9, refinamiento que el proyecto también está formalizando.

Lo que Lean no hace

Lean no comprueba que un enunciado sea el correcto ni el interesante. Comprueba que la prueba demuestre el enunciado tal como está escrito. Si alguien define mal un concepto, Lean demostrará fielmente un teorema sobre otra cosa. Por eso hay que revisar a mano las definiciones y el enunciado, mucho más cortos que la prueba.

Tampoco es infalible. El núcleo es software, y el software tiene errores. El 28 de julio de 2026 se notificó un error de solidez en el núcleo (issue #14576): un metaprograma malicioso podía conseguir que Lean aceptara una prueba de False, es decir, de cualquier cosa. El fallo apareció al analizar una supuesta «refutación» de la conjetura de Collatz hecha con ayuda de una IA. Se corrigió ese mismo día, en torno a una hora después, y la versión 4.32.2 lo arregla (según sus notas de versión). En su análisis posterior, De Moura lo calificó de «fallo de implementación, no un agujero en la metateoría de Lean» (an implementation bug, not a hole in Lean’s meta-theory). Para colar la prueba también ante nanoda, un verificador independiente, hacía falta además otro fallo distinto de este último: engañar a los dos exigía dos errores en dos implementaciones. Un núcleo pequeño se puede auditar y contrastar con verificadores independientes.

Por qué importa

Durante siglos, la garantía de una demostración fue la reputación de quien la revisaba. Con Lean aparece una segunda vía: que cualquiera compruebe, con un ordenador, que no falta ningún paso. Y queda una pregunta abierta y bonita: qué papel tendrá la IA cuando cada afirmación suya pueda ser revisada sin confiar en ella.

Practica: mira el algoritmo de Euclides en acción en RSA paso a paso, donde calcula la clave privada; es aritmética de números naturales como la que Mathlib tiene formalizada.

Fuentes

• Lean (about), Lean.
• Lean FRO About, Lean FRO (de aquí sale que De Moura creó Lean en 2013).
• Lean FRO, Lean FRO.
• Leonardo de Moura, Sebastian Ullrich (2021). The Lean 4 Theorem Prover and Programming Language, Conference on Automated Deduction (Springer).
• Lean community.
• The mathlib Community (2019). The Lean mathematical library, arXiv:1910.09336.
• Mathlib statistics (consultado el 15 de octubre de 2026), Lean community.
• Renaissance Philanthropy (2025). Lean FRO and Mathlib receive $10M from XTX Markets founder Alex Gerko.
• Peter Scholze (2020). Liquid Tensor Experiment, Xena Project.
• Lean community blog (2022). Liquid Tensor Experiment completed.
• W. T. Gowers, Ben Green, Freddie Manners, Terence Tao (2023). On a conjecture of Marton, arXiv:2311.05762.
• Terence Tao (2023). Formalizing the proof of PFR in Lean4 using Blueprint: a short tour.
• Lance Fortnow (2023). Do we need to formalize?
• W. T. Gowers, Ben Green, Freddie Manners, Terence Tao (2024). Marton’s Conjecture in abelian groups with bounded torsion, arXiv:2404.02244.
• Jyun-Jie Liao (2024). Improved Exponent for Marton’s Conjecture in F_2^n, arXiv:2404.09639.
• teorth/pfr, GitHub.
• Leonardo de Moura (2026). Postmortem for Kernel Soundness Bug #14576.
• Issue #14576 de lean4, GitHub (2026).
• Lean 4.32.2 release notes, Lean Reference Manual (2026).
• Lean release notes, Lean Reference Manual.