Estado del arte a agosto de 2026
Hay que distinguir tres cosas que la prensa confunde sistemáticamente:
La sinergia que define el momento actual es que (3) sin (1) no vale nada —sería otro generador de texto plausible— y (1) sin (3) es insoportablemente lento. El kernel de Lean es lo que convierte la matemática en un entorno de RL con verdad verificable, análogo al Go: recompensa binaria, sin ambigüedad, sin juez humano.
Filosóficamente, la pregunta interesante no es “¿puede la máquina demostrar?” sino dónde queda el residuo no mecanizable. Adelanto la tesis: se ha desplazado casi enteramente del proof al statement.
Lean 4 implementa una teoría de tipos dependientes de la familia del CIC (Coquand–Huet, extendido con familias inductivas por Paulin-Mohring). Los rasgos relevantes:
∀ n : ℕ, n + 0 = n es un tipo; su prueba es una función
que, dado n, produce un habitante de
n + 0 = n.Fin n (los naturales menores que n) es un tipo
indexado por un término. Esto es lo que permite enunciar teoremas sobre
estructuras arbitrarias de modo uniforme, y es lo que distingue a Lean
de Isabelle/HOL.Prop impredicativa
(Sort 0), con irrelevancia definicional de
pruebas: dos pruebas del mismo enunciado son
definicionalmente iguales. La prueba no es un objeto matemático
con contenido; es un testigo desechable.Type 0 : Type 1 : Type 2 : …, no
acumulativa, con polimorfismo de universos. La razón de la
jerarquía es exactamente la paradoja de Girard (la versión tipada de
Russell): Type : Type es inconsistente.Quot) como primitiva
del kernel, no como construcción derivada.El CIC puro es constructivo. Mathlib no lo es. Toda la matemática de mathlib descansa sobre tres axiomas añadidos:
| Axioma | Contenido |
|---|---|
propext |
Extensionalidad proposicional: proposiciones equivalentes son iguales |
Quot.sound |
Corrección del cociente |
Classical.choice |
Axioma de elección |
Por el teorema de Diaconescu, la elección implica el
tercio excluso. De modo que el sistema en el que efectivamente trabajan
los matemáticos en Lean es lógica clásica de orden superior
sobre teoría de tipos dependientes —no una lógica
intuicionista. La opción constructiva existe (#print axioms
permite auditar de qué axiomas depende cada teorema) pero es minoritaria
en la práctica matemática.
Esto tiene una consecuencia importante y poco advertida: Lean no es fundacionalmente neutral. La elección de CIC + elección + LEM es una decisión metafísica tomada por razones de ergonomía, no de principio.
Resultado clave (Carneiro, The Type Theory of Lean, tesis de maestría, CMU 2019; ampliado en el proyecto Lean4Lean):
Lean es equiconsistente con ZFC + {existen n cardinales inaccesibles | n < ω}.
Es decir: Lean prueba Con(ZFC), y por tanto —por el segundo teorema de Gödel— la consistencia de Lean no es demostrable en ZFC. La “verificación absoluta” que ofrece un asistente de pruebas está condicionada a un supuesto de cardinales grandes que no puede justificarse desde dentro.
La construcción del modelo es reveladora: por la irrelevancia de
pruebas y la elección, ⟦Prop⟧ := {∅, {•}} (el álgebra
booleana de dos elementos); y por los tipos inductivos, los universos
deben ser universos de Grothendieck, ⟦Uₙ₊₁⟧ = V_κₙ con κₙ
el n-ésimo inaccesible.
Grieta técnica que merece atención: Carneiro señala
que el juicio de tipado de Lean es “casi” decidible, pero no del
todo — por una interacción entre la eliminación de subsingletons
(para Acc) y la irrelevancia de pruebas. Lean resuelve esto
infraaproximando las relaciones ≡ y
⊢: el algoritmo implementado es más restrictivo que la
relación teórica. El verificador que corre en tu máquina no es el
sistema formal que la teoría describe, sino una aproximación
conservadora de él.
Los hammers (Lean-auto, LeanHammer, Duper) traducen objetivos de Lean a lógicas más pobres donde existen procedimientos de búsqueda eficientes:
El paso crítico es la monomorfización: eliminar polimorfismo y dependencia de tipos para obtener algo que un ATP entienda. La traducción está diseñada para ser sound (lo que prueba es verdadero), pero es necesariamente incompleta: los ATP no razonan con tipos dependientes. Luego un mecanismo de proof reconstruction reconstruye la prueba dentro del kernel de Lean, porque la palabra del ATP no se acepta.
Duper (Clune, Qian, Bentkamp, Avigad 2024) es la excepción interesante: un demostrador por superposición que trabaja nativamente en teoría de tipos dependientes y produce términos de prueba de Lean directamente, sin traducción a una lógica menos expresiva. Canonical ataca el problema dual: habitación de tipos en DTT.
Aquí no hay lógica en absoluto. El LLM es un generador de cadenas; la lógica está fuera, en el kernel. Dos modos:
AlphaProof (DeepMind, publicado en Nature, 2025) añade test-time RL: ante un problema difícil, genera millones de variantes del propio problema y aprende de ellas en tiempo de inferencia. Coste reportado: ~500 días-TPU por problema.
| Sistema | Lógica | Nota |
|---|---|---|
| Lean 4 | CIC + LEM + AC | dependiente, clásica, cocientes primitivos |
| Rocq (Coq) | CIC | constructiva por defecto |
| Isabelle/HOL | Teoría de tipos simple polimórfica | más débil, más automatizable (Sledgehammer) |
| Mizar | Teoría de conjuntos Tarski–Grothendieck | fundación conjuntista clásica |
| Agda / Cubical | MLTT / HoTT | univalencia, igualdad como estructura |
| Metamath | esquemas de primer orden | kernel minúsculo, sin tipos |
La elección de fundación determina qué es fácil. En HOL las categorías son incómodas; en HoTT los cocientes son gratis pero la matemática clásica es cara; en Lean los cocientes y la matemática clásica son gratis pero las estructuras superiores (∞-categorías) son casi imposibles. No hay fundación neutral: cada una hace visible una región y opaca otra.
Mathlib es la biblioteca comunitaria de Lean 4: aproximadamente 2,1 millones de líneas, con más de 170.000 teoremas y 80.000 definiciones. Es la mayor biblioteca de matemática formalizada que existe.
Su cobertura es excelente en licenciatura, sustancial en posgrado, puntual en investigación — y ese perfil, más que ningún ranking, es lo que define el mapa.
| Proyecto | Resultado | Nota |
|---|---|---|
| Liquid Tensor Experiment (2020–jul. 2022) | Teorema principal de los espacios vectoriales líquidos (Clausen–Scholze) | 18 meses; reto lanzado por Scholze; obligó a construir matemática condensada en Lean |
| PFR (nov. 2023) | Conjetura polinómica de Freiman–Ruzsa de Marton | ~3 semanas; Tao, Dillies, Mehta; estrenó el flujo blueprint |
| Carleson (jun. 2024–jul. 2025) | Convergencia p.c.t.p. de series de Fourier, en versión generalizada a espacios métricos doblantes | 14 autores principales + 14 colaboradores; una de las mayores colaboraciones |
| Sphere eversion | Principio h completo para relaciones diferenciales abiertas y amplias | Massot et al.; demostró que Lean maneja topología geométrica |
| PrimeNumberTheoremAnd | Teorema de los números primos (versión fuerte) | Kontorovich–Tao; completado con asistencia del agente Gauss (Math Inc., 2025) |
| Flypitch | Independencia de la hipótesis del continuo (forcing) | Han & van Doorn |
| Con(NF) | Consistencia de New Foundations de Quine | Wilshaw |
| Cap set problem | Solución de Ellenberg–Gijswijt | Dahmen, Hölzl, Lewis |
| Determinación de Borel | Teorema de Martin | requiere fragmento grande de ZFC |
| Equational Theories Project (2024–) | Grafo de implicaciones entre 4.694 leyes ecuacionales de magmas: 22 millones de implicaciones | Tao; crowdsourcing masivo + ATP clásicos |
| FLT (2024–2029) | Último teorema de Fermat, vía Khare–Wintenberger/Kisin | Buzzard & Taylor; financiado por EPSRC hasta sept. 2029 |
Cito el diagnóstico más franco disponible, del propio equipo que construye herramientas de autoformalización:
“mathlib cubre franjas amplias pero incompletas del paisaje matemático; mientras algunos dominios, como el álgebra o la teoría de categorías, están bien representados, quedan grandes lagunas en otros, como la geometría diferencial o las EDP. Como resultado, la mayor parte de la investigación matemática actual no puede formalizarse en Lean sin un trabajo preparatorio prohibitivamente costoso.” — Formalizing Mathematics at Scale, arXiv:2605.29955 (2026)
Geometría diferencial — parcialmente presente. Hay variedades con modelo, fibrados vectoriales suaves, corchete de Lie de campos, grupos de Lie y su álgebra de Lie, métricas de fibrado, variedades riemannianas básicas, existencia de curvas integrales y flujos locales (Rothgang, 2025). Falta: conexiones y curvatura en generalidad, teoría de Hodge, teoría de índice, teoría de bordismos (en curso), geometría simpléctica. Un proyecto reciente sobre variedades G₂ tuvo que trabajar “a un nivel de abstracción superior que no requiriera la infraestructura de geometría diferencial ausente” — es decir, reformular el problema para esquivar el hueco.
Ecuaciones en derivadas parciales — casi vacío. No hay teoría de Sobolev madura, ni teoría de regularidad general, ni EDP no lineales. Hay islas: regularidad interior de De Giorgi–Nash–Moser (Armstrong & Kempe, 2026), derivación de campo medio de la ecuación de Vlasov (2026). Nada parecido a un tratamiento sistemático.
Análisis numérico — prácticamente inexistente. Proyectos en curso autoformalizan libros de texto (Iserles, Butcher).
Teoría de representaciones y formas automorfas — se está construyendo desde dentro del proyecto FLT. Buzzard fue explícito: uno de los objetivos del proyecto es que Lean acabe entendiendo formas y representaciones automorfas, representaciones de Galois, teoremas de modularity lifting, teoría de cuerpos de clases, variedades de Shimura. Esto no existía antes de FLT.
Estructuras superiores — ∞-categorías, categorías derivadas en generalidad, stacks, teoría de homotopía superior. Aquí el obstáculo no es de esfuerzo sino estructural (§III.1).
Lagunas puntuales sorprendentes. Un trabajo de autoformalización de teoría de redes tensoriales (2026) documentó los huecos que encontró: la forma normal de Jordan no está en mathlib; tampoco el teorema de Burnside para álgebras de matrices, ni Perron–Frobenius para aplicaciones completamente positivas, ni el teorema del punto fijo de Brouwer en forma usable. Estos casos son instructivos: no son matemática difícil, son matemática que nadie ha formalizado todavía. La cobertura de mathlib es irregular por razones sociológicas, no lógicas. Refleja qué le interesó a quién.
Esta es la sección conceptualmente decisiva. Los obstáculos son de cuatro tipos irreducibles entre sí.
Es el más profundo. En teoría de tipos intensional, la igualdad no es un dato dado: es una decisión de diseño con consecuencias.
Para ∞-categorías el problema se agrava a un problema de coherencia infinito: hay que justificar la interpretación de la igualdad estricta de la teoría de tipos como homotopía en una (∞,1)-categoría. Las internal language conjectures siguen abiertas. Esto es precisamente lo que la teoría homotópica de tipos y las fundaciones univalentes intentan resolver — y por eso la matemática de Lurie y Scholze es formalizable solo en fragmentos elegidos con cuidado.
Lectura filosófica: la identidad, que en la práctica matemática informal es transparente e invisible, se vuelve el obstáculo central en cuanto se exige explicitud. Lo “obvio” no es una propiedad del objeto sino un efecto de una práctica que no se examina a sí misma.
Macbeth lo ha formulado bien: el matemático humano ve los reales simultáneamente como clases de sucesiones de Cauchy, como cortaduras de Dedekind y como el único cuerpo arquimediano uniformemente completo, y desliza entre las tres sin fricción. El ordenador obliga a elegir una y quedarse en ella.
El proyecto Carleson documenta esto con precisión quirúrgica: hubo
que distinguir tres tipos de reales — ℝ,
ℝ≥0 y ℝ≥0∞ (extendidos) — porque en teoría de
la medida las integrales quieren vivir en los extendidos no negativos.
Un término x : ℝ≥0 no es un término de
tipo ℝ. Toda la formalización arrastra la tensión de
decidir en cuál de los tres poner cada constante, cada conjunto, cada
integrando.
En el LTE, el trabajo real no fue probar el teorema: fue construir los conjuntos condensados — reemplazar la noción de espacio topológico por la de haz sobre una categoría de espacios compactos Hausdorff. La formalización obligó a fijar una ontología antes de poder decir nada.
El factor de de Bruijn (van Benthem Jutting 1977; refinado por Wiedijk) mide el cociente entre el tamaño de la prueba formal y el de la informal. Estimaciones recientes en Isabelle dan valores de 13 a 25 para resultados de teoría de números. Los factores altos aparecen sistemáticamente donde hay que rellenar argumentos intermedios que el texto original daba por hechos.
Buzzard lo formuló con humor exacto en el blueprint de FLT:
“Nuestra tarea puede compararse con enseñar un curso de posgrado sobre el último teorema de Fermat a un ordenador. El ordenador es un miembro del público bastante exigente — insistirá en que se le den todos los detalles técnicos de todos los argumentos, y no aceptará pruebas por intimidación ni por apelación a la autoridad.”
El punto crucial: el ordenador solo empieza a rellenar detalles por sí mismo cuando los argumentos son matemáticamente obvios de forma absoluta. La zona intermedia —lo que un experto considera rutinario pero no trivial— es exactamente donde se va todo el tiempo. Y es exactamente la zona donde vive la práctica matemática real.
Este es el obstáculo del que no se sale, y el que más importa filosóficamente.
“Mientras los sistemas mencionados se apoyan en el compilador de Lean para proporcionar verdad-terreno absoluta para la verificación de pruebas, la autoformalización de enunciados plantea un reto distinto: no hay oráculo mecánico que confirme que un enunciado formal se corresponde con su contraparte informal.” — Beyond the Library, arXiv:2606.31134 (2026)
Consecuencias medidas:
Esta es la grieta estructural del programa entero: la formalización puede mecanizar la corrección de la inferencia, pero no la adecuación del enunciado. El juicio de que “esto que he escrito en Lean dice lo que yo quería decir” es irreductiblemente informal, humano y no verificable por el sistema. La cadena de verificación no se cierra sobre sí misma.
theorem add_zero (n : ℕ) : n + 0 = n := rflrfl es reflexividad: la igualdad se cumple
definicionalmente por la definición recursiva de la suma. El
kernel comprueba tipos, no busca.
El teorema generalizado se enuncia sobre un espacio métrico de medida
doblante arbitrario, con siete parámetros asociados
(a, q, K, σ₁, σ₂, F, G). La solución de ingeniería fue una
clase de tipos [ProofData a q K σ₁ σ₂ F G] en la que todos
los datos adicionales se asocian automática y unívocamente al espacio
X mediante outparams, de modo que el usuario nunca
tiene que darlos explícitamente. Es la mecanización del “sea fijado de
una vez por todas” del texto matemático.
La prueba informal ocupaba 30 páginas. El blueprint formal tiene 11 secciones, diseñado explícitamente para que un no experto pueda tomar un lema aislado y formalizarlo sin entender el conjunto. Esa modularidad es lo que hace posible la colaboración masiva.
El proyecto de Tao mapea implicaciones entre 4.694 leyes ecuacionales de magmas: 22 millones de pares. Detalle crítico, en palabras del propio Tao:
No se formalizan explícitamente en Lean los 22 millones de implicaciones, porque el tiempo de compilación sería prohibitivo. Solo se formaliza un conjunto mucho menor de (anti-)implicaciones, del que las demás se siguen por transitividad y dualidad, razonando fuera de Lean.
Es decir: el resultado publicitado como “22 millones de problemas resueltos con verificación formal” es, estrictamente, un conjunto formalizado de generadores más un argumento meta-nivel de clausura que no está en el kernel. Tao lo dice abiertamente y planea refactorizar. Pero la estructura es la que importa: incluso en el proyecto de formalización más ambicioso, hay un paso que se hace sobre el sistema y no dentro de él, por razones de coste computacional.
El proyecto no formaliza la prueba de Wiles/Taylor–Wiles de los 90 sino una prueba moderna (Khare–Wintenberger, Kisin, Taylor, Scholze). La razón es estratégica: el objetivo declarado no es solo llegar a FLT sino dotar a Lean del vocabulario de la teoría de números moderna. Antes de poder enunciar el teorema en la forma que se va a demostrar, hay que construir: curvas elípticas, representaciones de Galois, formas automorfas, teoría de cuerpos de clases, teoremas de dualidad aritmética, variedades de Shimura. La formalización precede a la demostración, y es el 90% del trabajo.
| Área | Por qué resiste |
|---|---|
| ∞-categorías, ∞-topos | Coherencia infinita; la igualdad estricta de Lean no modela homotopía |
| EDP no lineales | Falta infraestructura (Sobolev, regularidad); las pruebas son estimaciones densas de “epsilon-management” que no se comprimen |
| Geometría con diagramas | Argumentos que dependen de una figura no tienen forma canónica de formalización; hay que reconstruir el contenido |
| Análisis numérico | Nadie lo ha hecho; combina análisis real con aritmética de punto flotante |
| Matemática experimental / conjetural | No hay teorema que verificar |
| Teoría de modelos de estructuras concretas | Interacción de metateoría y teoría objeto, difícil de estratificar |
| Benchmark | Nivel | Mejor resultado |
|---|---|---|
| miniF2F | olimpiada / preuniversitario | 88,9% (DeepSeek-Prover-V2-671B) — saturado |
| PutnamBench | licenciatura | 87,9% (Seed-Prover 1.5); AlphaProof 56% con ~500 días-TPU/problema |
| FATE-H | álgebra de posgrado | 80% (Seed-Prover 1.5); 71% (DeepSeek-R1, informal) |
| FATE-X | exámenes de calificación de doctorado | 33% |
| FrontierMath Tier 4 | investigación real | 18,75% (Gemini 3 Pro); estimaciones más optimistas hasta 40% |
La curva es inequívoca y su forma también: se colapsa exactamente donde empieza la matemática de investigación. Seed-Prover 1.5 lo reconoce en su propio informe: el sistema “sigue enfrentando dificultades con problemas de nivel doctoral y superiores”.
DeepMind hizo un barrido sobre problemas de Erdős con agentes autónomos. De 200 soluciones candidatas marcadas como correctas o incorrectas, solo el 6,5% eran “significativamente correctas” (Feng et al., 2026). Cuatro problemas de Erdős fueron resueltos autónomamente en diciembre de 2025 — un resultado real y notable. Pero la tasa de señal frente a ruido en el régimen de investigación abierta es del orden del 5%.
Esto explica por qué la formalización importa más, no menos, con IA capaz: cuanto más plausible es el texto generado, más necesario es un verificador que no se deje convencer.
Un experimento de 2026 (Formalizing Mathematics at Scale) aplicó un agente autoformalizador a 26 libros de texto de acceso abierto —análisis real, complejo, funcional, Fourier, diferencial; álgebra abstracta y teoría de Lie; geometría algebraica y diferencial; topología algebraica; teoría de números; combinatoria; EDP; probabilidad—, con intervención humana mínima (a veces nula, a veces unos mensajes al día del tipo “prueba a descomponer esto en lemas auxiliares”), aproximadamente una semana por libro. Resultado: más de 45.000 declaraciones de Lean 4 verificadas.
La lectura correcta de esto es matizada. La anchura se está automatizando muy deprisa: rellenar el sustrato de licenciatura y posgrado temprano que faltaba en mathlib es hoy una tarea de máquina. La profundidad no: FLT sigue teniendo horizonte 2029 con financiación dedicada y decenas de expertos humanos.
Este material ofrece un caso de estudio inusualmente limpio, porque aquí la aporía no es especulativa: está documentada por los propios practicantes, con números.
El argumento estándar a favor de la formalización es que reemplaza la confianza social (en el árbitro, en la comunidad, en la reputación) por certeza mecánica. Lo que ocurre en realidad es un desplazamiento del punto de confianza, no su eliminación:
Lean4Lean —verificar el verificador de Lean en Lean— es la respuesta natural y también la ilustración perfecta del problema: es un movimiento autorreferencial que no puede cerrar. Los autores lo señalan: es improbable que se pueda probar la terminación del verificador de Lean dentro de Lean. La estructura es gödeliana, no por analogía retórica sino por la misma razón matemática.
Formulación de la aporía: la formalización se presenta como el cierre del regreso de justificación en matemática. Lo que produce es un regreso más corto, más explícito y mejor documentado — pero abierto en los dos extremos: hacia arriba en la fidelidad semántica del enunciado, hacia abajo en la consistencia del sistema.
En la práctica informal, la identidad es transparente: “los reales” son los reales, se entren por Cauchy o por Dedekind. En cuanto se exige explicitud, la identidad se revela como el problema técnico central (§III.1) y como una elección con consecuencias irreversibles. El resultado de Palmgren —no hay extensión general a igualdad de objetos sin UIP— es un resultado de imposibilidad estructural, no una dificultad de implementación.
Esto conecta directamente con la línea Leibniz–Frege–Wittgenstein sobre la identidad, y con la propuesta univalente (Voevodsky) de que la identidad sea la equivalencia. Que existan fundaciones alternativas incompatibles, cada una haciendo fácil lo que la otra hace imposible, es un caso de subdeterminación metafísica exactamente del tipo que el marco de las grietas identifica en la individuación cuántica: los datos (la matemática que queremos formalizar) no determinan la fundación.
Es el eje de la crítica filosófica seria, y hay literatura de calidad:
El propio Carleson lo ilustra: la reconstrucción de prueba de los hammers produce, según sus autores, “una prueba demasiado grande para leerse, y por tanto no se sugiere como sustituto de la invocación de la táctica”. El objeto formal correcto y el objeto epistémicamente valioso se han separado.
Sintetizando §III.4 en la forma que interesa al manuscrito:
El programa de formalización pretende que la corrección matemática sea decidible. Lo consigue —para el paso deductivo. Pero para hacerlo necesita un enunciado formal, y la adecuación del enunciado formal a la intención matemática no es formalizable, por razones de principio y no de tecnología: formalizarla requeriría un enunciado formal de la adecuación, que a su vez requeriría verificar su propia adecuación.
Es exactamente la estructura del regreso, y es la razón por la que los papers de 2026 introducen “Faithfulness Judges” — otro LLM que juzga si el Lean dice lo que dice el texto. Un juez no verificable vigilando a un traductor no verificable, ambos apuntalando un verificador que sí lo es. La certeza mecánica descansa sobre una capa irreductiblemente hermenéutica.
Esto es formulable como aporía en el esquema del manuscrito:
Documento elaborado en agosto de 2026. La velocidad de cambio en la sección V (benchmarks e IA) es alta: los números citados envejecen en meses. Las secciones I, III y VI son estructurales y estables.