Cómo funciona Lean, el programa que no se fía de quien demuestra

El 4 de septiembre, Anthropic publicó la primera demostración completa del último teorema de Fermat comprobada por ordenador. El teorema dice que no existen números enteros positivos a, b y c tales que aⁿ + bⁿ = cⁿ cuando n es mayor que 2. Fermat lo anotó hacia 1637 en el margen de un libro, y Andrew Wiles publicó la primera demostración correcta en 1995, después de más de 350 años de intentos fallidos.

Anthropic no ha encontrado una demostración nueva. Ha reescrito la de Wiles, en la versión expuesta por Darmon, Diamond y Taylor, en un lenguaje llamado Lean. Lo hicieron decenas de agentes de Claude durante 11 días, con indicaciones humanas ocasionales. El resultado ocupa 13 millones de líneas: más de cinco veces el tamaño de Mathlib, la gran biblioteca de matemáticas comprobadas que mantiene la comunidad.

Nadie va a leer 13 millones de líneas. Aun así, Kevin Buzzard, el matemático del Imperial College de Londres que dirige desde 2024 el proyecto comunitario para formalizar esa misma demostración, la revisó y concluyó que prueba el teorema sin más suposiciones que los axiomas de las matemáticas.

Cinco días después, la empresa de seguridad Trail of Bits publicó otra «demostración» de Fermat. Esta cabía en una pantalla, y Lean también la marcaba como correcta.

Las dos cosas son ciertas, y entender por qué es entender cómo funciona Lean. En el artículo sobre las 722 demostraciones de OpenAI separamos las capas de lo que significa que un resultado esté «comprobado». Aquí miramos dentro de la primera: qué hace exactamente el programa, qué parte hay que creerse y qué ha pasado este año cuando esa parte ha fallado.

Una demostración que compila

Lean es a la vez un lenguaje de programación y un asistente de demostraciones: un programa en el que se escribe una demostración con tanto detalle que el ordenador puede revisar cada paso. Lo empezó Leonardo de Moura en Microsoft Research en 2013, y desde 2023 lo desarrolla Lean FRO, una organización sin ánimo de lucro creada para ese fin.

La forma más rápida de entender qué hace es darle dos afirmaciones sencillas, una cierta y una falsa:

example : 2 + 2 = 4 := rfl

example : 2 + 2 = 5 := rfl

Type mismatch
  rfl
has type
  ?m.16 = ?m.16
but is expected to have type
  2 + 2 = 5

El error dice type mismatch, un desajuste de tipos: el mismo error que da un compilador cuando se pasa un texto donde se esperaba un número. No es una coincidencia de vocabulario. En Lean, una afirmación es un tipo y una demostración es un valor de ese tipo. Comprobar una demostración consiste en comprobar que el valor tiene el tipo correcto, igual que un compilador comprueba que una función devuelve lo que dice devolver.

Esta equivalencia entre demostraciones y programas se conoce como «proposiciones como tipos» o correspondencia de Curry-Howard. La fueron descubriendo los lógicos entre los años treinta y sesenta del siglo pasado, y es la base de Lean y de otros asistentes como Rocq o Agda. Para quien programa, la consecuencia es fácil de imaginar: que una demostración sea correcta significa que compila.

Escribir una demostración es conversar con Lean

Casi nadie escribe esos valores a mano. Lo habitual es usar tácticas: órdenes como «haz inducción» o «reescribe usando esta igualdad», que van transformando lo que queda por demostrar. En cada paso, Lean enseña el estado de la demostración: qué datos tenemos y qué objetivo falta, marcado con el símbolo ⊢.

Un ejemplo completo: demostrar que sumar cero por la izquierda deja igual a un número natural. Parece obvio, pero en Lean no lo es. La suma está definida recorriendo el segundo número, así que n + 0 = n sale directamente de la definición, mientras que 0 + n = n hay que demostrarlo.

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

n : Nat
⊢ 0 + n = n

k : Nat
ih : 0 + k = k
⊢ 0 + (k + 1) = k + 1

⊢ 0 + k + 1 = k + 1

Lo interesante es lo que pasa cuando un paso falla. Si nos saltamos el reagrupamiento y escribimos directamente rw [ih], Lean no se limita a decir que no:

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  0 + k
in the target expression
  0 + (k + 1) = k + 1

Dice qué buscaba, dónde lo buscaba y en qué estado se ha quedado. Esta conversación, en la que cada paso recibe una respuesta inmediata y precisa, explica buena parte de por qué Lean se ha convertido en uno de los entornos más usados por los sistemas de IA que hacen matemáticas. Volveremos a ello.

Debajo de las tácticas hay un programa

Las tácticas no son la demostración: son programas que la construyen. Si le pedimos a Lean que enseñe lo que ha guardado como cero_mas, aparece esto:

theorem cero_mas : ∀ (n : Nat), 0 + n = n :=
fun n =>
  Nat.recAux (Eq.refl (0 + 0))
    (fun k ih =>
      Eq.mpr (id (congrArg (fun _a => _a = k + 1) (Eq.symm (Nat.add_assoc 0 k 1))))
        (Eq.mpr (id (congrArg (fun _a => _a + 1 = k + 1) ih)) (Eq.refl (k + 1))))
    n

Es una función que, para cada n, construye la prueba por recursión encadenando igualdades. Nadie lo escribe así; lo generan las tácticas. Y es este objeto, llamado término de prueba, el que se comprueba.

Esa separación es la decisión de diseño más importante de Lean. Las tácticas pueden ser tan sofisticadas como se quiera. Hay tácticas que resuelven solas problemas de aritmética, como omega, o que buscan combinaciones de hechos conocidos, como grind, y cualquiera puede escribir las suyas. Ninguna necesita ser correcta. Todo lo que producen acaba convertido en un término como el de arriba, y ese término lo revisa un componente pequeño llamado núcleo (kernel, en inglés), que solo conoce las reglas básicas de la lógica de Lean. Si una táctica tiene un error y construye algo inválido, el núcleo lo rechaza. La guía oficial para validar una demostración cuenta los errores de las tácticas entre lo que ya queda cubierto con solo compilar.

La idea de que una maquinaria grande produzca resultados y un comprobador pequeño los revise se conoce como criterio de De Bruijn, por el matemático neerlandés que la puso en práctica en su sistema Automath a finales de los años sesenta.

Esta separación es decisiva para la inteligencia artificial. Un modelo de lenguaje es, para Lean, una táctica más: algo que propone pasos. Puede inventarse un lema, tomar un camino absurdo o generar trece millones de líneas. Lean no necesita fiarse de él, igual que no se fía de la persona que escribe ni de omega.

Tres axiomas y un sorry

Que el núcleo acepte algo no basta para saber qué se ha demostrado. Lean permite trabajar con huecos y con suposiciones, y ambos son fáciles de pasar por alto.

El hueco se llama sorry: una palabra que se escribe en lugar de una demostración pendiente. Lean la acepta para que se pueda avanzar por partes, pero avisa y deja constancia. Las suposiciones son los axiomas, afirmaciones que se aceptan sin demostración. Lean trae tres de serie, que la práctica matemática habitual da por buenos aunque tengan nombres poco amigables:

• propext: dos afirmaciones que se implican la una a la otra son la misma afirmación.
• Quot.sound: se pueden tratar como un solo objeto todos los que consideramos equivalentes. Es la operación con la que se construyen, por ejemplo, las fracciones a partir de parejas de enteros, donde 1/2 y 2/4 son el mismo número.
• Classical.choice: de un conjunto que no está vacío se puede elegir un elemento, aunque no sepamos cuál. Es el axioma de elección.

Pero cualquiera puede añadir más, incluidos axiomas falsos. Por eso la orden más importante para revisar una demostración ajena no es compilarla, sino preguntarle a Lean de qué depende, con #print axioms. Con nuestros ejemplos:

theorem trampa : 2 + 2 = 5 := by sorry

theorem cero_mas' (n : Nat) : 0 + n = n := by
  omega

'cero_mas' does not depend on any axioms
'cero_mas'' depends on axioms: [propext, Quot.sound]
'trampa' depends on axioms: [sorryAx]

La guía de la comunidad para saber si algo está demostrado pide justo eso: que la respuesta no incluya nada fuera de esos tres axiomas. El repositorio de Fermat lo convierte en una condición para compilar:

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n

/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms fermat_last_theorem

La «demostración» que cabía en el margen

Ahora se entiende el truco de Trail of Bits. Su demostración usaba native_decide, una táctica que, para ir más rápido, no deja que el núcleo haga un cálculo, sino que lo ejecuta como código compilado. Es útil para cálculos grandes, pero tiene un precio: además del núcleo, hay que fiarse del compilador. Lean lo registra añadiendo un axioma a la lista.

El código compilado de una función tenía un error. La función que extrae un trozo de un texto daba resultados distintos según se razonara sobre ella o se ejecutara. Si se pedía un fragmento a partir de una posición astronómicamente grande, su definición lógica devolvía un texto vacío, mientras que el código compilado devolvía el texto entero. Trail of Bits usó las dos respuestas para concluir que un texto vacío era igual a uno que no lo estaba. Y de una contradicción se puede deducir cualquier cosa, también el teorema de Fermat.

El editor mostraba las marcas azules de «correcto». Pero #print axioms añadía a los tres estándar uno más: flt._native.native_decide.ax_1_1. La propia Trail of Bits aclaró que no era un fallo del núcleo. El equipo de Lean corrigió la parte más grave en unas tres horas y el resto, cinco días después. El error afectaba a todas las versiones estables hasta la 4.33.1, justo la que usa el repositorio de Fermat de Anthropic. Ese proyecto no está afectado: prohíbe native_decide y exige exactamente los tres axiomas.

La lección es práctica. El veredicto no es la marca azul del editor, sino la lista de axiomas. La guía oficial lo dice expresamente: las marcas azules aparecen aunque una de las piezas en las que se apoya el teorema use sorry, y un axioma con _native en el nombre indica que parte del cálculo lo ha hecho código compilado.

¿Y si el que falla es el núcleo?

El núcleo es pequeño, pero no infalible, y en julio se demostró.

El 25 de julio, Ramana Kumar publicó una refutación de la conjetura de Collatz obtenida con ayuda de IA. La conjetura dice que, si se toma cualquier número entero positivo y se divide por dos cuando es par o se multiplica por tres y se le suma uno cuando es impar, tarde o temprano se llega al 1. La refutación no tenía ningún sorry. Tampoco era válida: aprovechaba un error del núcleo al manejar tipos inductivos anidados, que son tipos definidos en términos de sí mismos dentro de otros, como un árbol cuyas ramas son una lista de árboles.

El 28 de julio, Kiran Gopinathan la redujo a una demostración de «falso» y la notificó. Una hora después había una corrección, publicada en Lean 4.32.2. La demostración de Fermat se compiló con la 4.33.1, que ya la incluye. Según el análisis posterior de Leonardo de Moura, el fallo solo era alcanzable mediante metaprogramación, es decir, con programas que envían declaraciones directamente al núcleo sin pasar por las comprobaciones habituales.

La parte más instructiva es la segunda comprobación. Como el núcleo puede fallar, existen núcleos independientes: programas escritos desde cero que vuelven a revisar los mismos términos. El principal es nanoda, escrito en Rust por Chris Bailey. La refutación de Kumar también había pasado una versión de nanoda de una semana antes, porque aprovechaba a la vez otro error, distinto y ya corregido, de nanoda. Hicieron falta dos errores sin relación en dos implementaciones a la vez. La conclusión de De Moura es que la comprobación independiente sigue funcionando, siempre que se usen versiones actualizadas de ambos. Después, un investigador de OpenAI, con ayuda de una IA especializada en seguridad, encontró más errores en el núcleo, todos alcanzables solo por metaprogramación. El comprobador nanoda los detectó todos.

Lean FRO ya ponía a prueba en público los comprobadores independientes en la Lean Kernel Arena, y tras julio ha añadido allí las pruebas de estos errores y se ha comprometido a invertir en más implementaciones. El comprobador más llamativo es con-leche, publicado en septiembre: un comprobador externo acompañado de una demostración, escrita en Lean, de que nunca acepta una prueba de «falso». Su README cuenta que lo implementó y demostró Claude, bajo la supervisión de Joachim Breitner, de Lean FRO, que describe el código como un montón desordenado que funciona y está demostrado. No elimina toda la circularidad, porque esa demostración la revisa a su vez un núcleo de Lean, pero un error tendría que colarse en piezas que funcionan de forma distinta.

La guía oficial de Lean ordena todas estas comprobaciones de menos a más exigente. Cada nivel añade protección, pero también deja algo fuera:

Fuente: «Validating a Lean Proof», manual de referencia de Lean. Resumen de Codin. La guía reserva el último nivel para situaciones de alto riesgo, como competiciones con premio o sistemas de IA de los que no se puede dar por hecho que actúan de buena fe.

La demostración de Fermat de Anthropic pasó por el último: el núcleo oficial, una versión de nanoda que revisó 1.052.234 declaraciones sin errores y Comparator, la herramienta que verifica en un entorno aislado que el enunciado demostrado es idéntico al de referencia. Eso no es certeza absoluta. Es otra cosa: confiar en algo pequeño, público y comprobado de varias formas.

Lo que ningún programa revisa

El núcleo garantiza que el término demuestra el enunciado escrito. No garantiza que ese enunciado diga lo que creemos. La guía de la comunidad pone ejemplos: se puede redefinir qué son los números naturales, o llamar TheRiemannHypothesis a cualquier afirmación, y demostrar algo que se parece a un gran teorema sin serlo.

El enunciado de Fermat está escrito con los números naturales y las operaciones que trae Lean. Solo la potencia viene de Mathlib, y Comparator comprueba que coincide con el enunciado que Mathlib ya tenía, revisado por sus responsables. Por eso es fácil confiar en él. Lo que no puede comprobar ninguna herramienta, advierte el propio repositorio, es que cada uno de los 29.511 teoremas intermedios signifique lo que sugiere su nombre. Para el resultado final da igual, porque el núcleo revisa todo lo que hay por debajo. Para que una persona aprenda algo de esa demostración, no.

Aquí está la función menos visible de Mathlib. A 8 de octubre de 2026 reúne 290.229 teoremas y 137.964 definiciones de 772 personas. Su valor no es solo la cantidad: son definiciones compartidas y revisadas, sobre las que un enunciado nuevo se puede leer sin desconfiar de cada palabra. Cuando un resultado necesita definiciones que Mathlib no tiene, alguien del área tiene que revisarlas, como explicamos con los casos de OpenAI que se apoyaban en definiciones propias.

Por qué a la IA le sienta tan bien

Volvamos a la conversación del principio. Lean responde a cada paso con precisión, y su veredicto final es un sí o un no que no se puede discutir sonando convincente. Para un sistema de IA, es un entrenador ideal. En el repaso de lo que ha hecho mejorar a los modelos de lenguaje explicamos cómo entrenar con recompensas que se pueden comprobar cambió su forma de razonar. Lean lleva esa idea al extremo.

AlphaProof, de Google DeepMind, es el ejemplo más documentado. Según su artículo en Nature, publicado en noviembre de 2025, aprendió a buscar demostraciones en Lean por aprendizaje por refuerzo, con un método inspirado en AlphaZero y millones de problemas traducidos automáticamente a Lean. Junto con AlphaGeometry 2, obtuvo en la Olimpiada Internacional de Matemáticas de 2024 una puntuación equivalente a una medalla de plata. Anthropic cuenta algo parecido en otra dirección: Claude usa demostraciones parciales en Lean para comprobar sus propias hipótesis mientras trabaja, igual que usaría una simulación numérica para ver si va bien encaminado.

Ese mismo rigor tiene una consecuencia incómoda. Un sistema que se optimiza para que Lean diga que sí encontrará los agujeros de Lean si los hay. La refutación de Collatz se obtuvo con ayuda de IA. Joachim Breitner apuntó que quizá no era casualidad que los dos errores aparecieran casi a la vez: ya hay modelos capaces de encontrarlos. La guía oficial de Lean, de hecho, pone las demostraciones generadas por IA sin revisar en el mismo grupo que las que intentan engañar a propósito. Cuanto mejores son los sistemas que generan, más importa que el comprobador sea pequeño, revisado y redundante.

Comprobar tampoco es gratis. La demostración de Fermat costó unos 6.000 millones de tokens de salida y varios intentos fallidos antes de que una plataforma de coordinación, Prove2Me, mantuviera ordenado el trabajo de los agentes. Repetir la comprobación es mucho más barato que revisarla a mano, pero no trivial: según el repositorio, compilarla llevó cinco horas y media con 96 procesos en paralelo, y Comparator, casi quince horas con picos de 230 GB de memoria.

El mismo reparto, fuera de las matemáticas

Lo que Lean organiza para las matemáticas ya se usa para software en producción.

En AWS, el equipo de Cedar, el lenguaje con el que se escriben las políticas de autorización (quién puede hacer qué sobre qué recurso), mantiene un modelo de cada componente en Lean, unas diez veces más pequeño que el código real en Rust. Demuestra propiedades de seguridad sobre ese modelo y genera millones de entradas aleatorias para comprobar que el modelo y el código responden lo mismo. Según el caso publicado por Lean, no sale ninguna versión nueva de Cedar si el modelo, las demostraciones y esas pruebas no están al día.

En Microsoft, SymCrypt, la biblioteca criptográfica que usan Windows y Azure, escribe sus algoritmos nuevos en Rust, los traduce a Lean con una herramienta llamada Aeneas y demuestra que cumplen especificaciones derivadas de los estándares del NIST. En julio publicó las primeras demostraciones completas: ML-KEM, un algoritmo para intercambiar claves resistente a ordenadores cuánticos, y SHA-3. El esquema con el que lo explican reparte el trabajo en tres. Los agentes de IA, que llaman estocásticos, escriben las demostraciones. Las herramientas, deterministas, compilan, traducen y comprueban. Y las personas dedican su atención a revisar cómo se han formalizado los estándares y qué propiedades importan.

Ese reparto es lo más transferible de Lean para cualquier equipo que meta IA en un proceso, aunque nunca vaya a escribir una demostración. La generación puede ser abundante y poco fiable si se cumplen tres condiciones. Lo que comprueba es pequeño, determinista e independiente de lo que genera. Se sabe exactamente qué se ha dado por supuesto, el equivalente a #print axioms: qué pruebas se han saltado, qué se ha simulado, qué se ha aceptado sin revisar. Y las personas revisan la especificación, que es la parte que ninguna máquina puede validar por ellas. Los tests y los sistemas de tipos son versiones débiles de la misma idea; Lean es su versión extrema.

Lean no se fía de quien demuestra, sea una persona, una táctica o un modelo. Nosotros sí tenemos que fiarnos de algo. Lo que ha cambiado es su tamaño: ya no es la reputación de un autor ni una revisión de años, sino un núcleo pequeño, tres axiomas y un enunciado que cabe en dos líneas. La pregunta útil deja de ser cuánto confiamos en el modelo y pasa a ser qué es lo mínimo que tenemos que creernos y quién lo ha revisado.

Fuentes

• Anthropic: «Formalizing Fermat’s Last Theorem», 4 de septiembre de 2026 y repositorio anthropics/fermats-last-theorem, consultado el 8 de octubre de 2026.
• Trail of Bits: «A “proof” of Fermat’s Last Theorem that fits the margin», 9 de septiembre de 2026.
• Leonardo de Moura: análisis del fallo del núcleo #14576, 1 de agosto de 2026 y notas de Lean 4.32.2, 28 de julio de 2026.
• con-leche: comprobador externo de Lean con demostración de consistencia y Lean Kernel Arena.
• Comunidad de Lean: «Did you prove it?» y estadísticas de Mathlib, consultadas el 8 de octubre de 2026.
• Lean FRO: historia y organización y manual de referencia de Lean: «Validating a Lean Proof».
• Hubert et al.: «Olympiad-level formal mathematical reasoning with reinforcement learning», Nature, noviembre de 2025.
• Lean: caso de Cedar en AWS y AWS Open Source Blog: «Lean into verified software development».
• Microsoft Research: «Verifying Rust cryptography in SymCrypt, from standards to code», 13 de julio de 2026.
• Los ejemplos de código propios se probaron en el editor web oficial de Lean con la versión v4.35.0-rc4.