El que propone, el que verifica, y la capa de en medio

Qué es. Un traductor con verificador: convierte una pregunta en lenguaje natural en un enunciado de Lean 4 y somete ese enunciado al kernel. Lo que devuelve no es una respuesta sino un veredicto, y el código que lo sostiene.

Por qué hace falta. Un modelo de lenguaje que responde matemáticas produce texto plausible. La plausibilidad no es una demostración, y el modelo no distingue entre las dos: escribe con la misma seguridad un lema que existe y uno que ha inventado. De 28 identificadores que propuso de memoria, 21 no existían —y los 21 eran lemas, con la convención de nombres de Mathlib seguida al dedillo—. Por eso la decisión sobre qué es cierto se saca del modelo y se entrega al kernel de Lean 4, que sólo acepta lo que puede comprobar.

Eso reparte el trabajo en tres papeles que no se solapan:

Las tres vueltas del lazo, y dónde se cierra cada una

«El modelo propone y Lean evalúa» es la forma; lo que la hace funcionar es qué vuelve, y hasta dónde. El sistema cierra tres lazos de radio distinto, y ninguno de los tres es el modelo hablando consigo mismo:

Las tres vueltas operan sobre un objeto que el grafo de conceptos no contiene: el estado de prueba. Ese objeto tiene su propia categoría, construida y medida (§8) — objetos los estados, morfismos las tácticas, no goals el objeto terminal. Y el sistema enseña las tres vueltas al alumno en vez de resumírselas: el panel de explicabilidad dice qué se entendió, qué se activó, qué capacidades corrieron y cuáles no —con su motivo—, y qué contestó Lean en cada ronda.

Y una segunda regla, sobre la evidencia

Cada componente del núcleo lleva una medición con su modelo nulo al lado. Un porcentaje solo no dice nada: un clasificador que acierta el 61 % parece bueno hasta que se comprueba que responder siempre lo mismo acierta el 89 %. Comparar dos versiones de la propia idea tampoco es medir — es preferir.

La consecuencia es que este documento contiene componentes que no baten a su nulo, y lo dice. Tres de ellos están apagados en producción por esa razón, mediante una regla explícita (§12), no por criterio de nadie.

Todo pasa por Nucleo.process(texto). Son seis pasos entre dos fronteras de idioma. El núcleo interviene en tres de los seis; en ninguno decide si algo es cierto.

La última columna es el resultado de medir cada punto por separado. No hay un veredicto único sobre «el núcleo»: aporta en el paso 1 y en el paso 5 —y por razones distintas, a un lado y a otro de la frontera de formalización (§5)—, y en el 3 lo que va siempre es el módulo del nombre que se ofreció. Resumirlo en una sola cifra sería mentir por agregación.

Esta tabla tenía dos filas más. Proponer módulos vecinos además de los del nombre ofrecido empataba con un conjunto fijo de tres —18 de 20 enunciados elaboran, los mismos— y la regla por área que ordenaba la cascada perdía contra «probar simp primero» —1,262 contra 1,091—. Las dos estaban apagadas por el decisor y el 21 de septiembre de 2026 se quitaron del código; su cifra queda en §16. Lo que ordena la cascada hoy es un clasificador sobre la forma del objetivo, que es otra cosa y se mide aparte.

El alumno pregunta en castellano y todo el aparato del sistema es inglés: las palabras clave del grafo, los 183 433 hechos de Mathlib, los ejemplos few-shot de miniF2F y el propio Lean. Quien escribe «¿Es 17 un número primo?» no toca ninguna de esas palabras.

La consulta se traduce una sola vez, al entrar, con un modelo local de 74 M de parámetros (Helsinki-NLP/opus-mt-es-en): sin API y sin coste por consulta. El inglés pasa directo.

$x^2 - 5x + 6$          →  $x^2 - 5x + $6
\mathbb{R}$             →  \mathbb{R$
\int_0^\infty ... dx$   →  int_0=infty ... dx$    (destruido)
\sin x                  →  \without x

Y la frontera se cruza de vuelta. Si preguntó en castellano, la respuesta sale en castellano, y eso hay que fijarlo explícitamente en el prompt: el enunciado que el modelo tiene delante ya está en inglés, así que una instrucción como «responde en el idioma del usuario» le haría contestar en inglés. Lo que se le enseña como «pregunta original» es la del alumno, no la traducción, y el historial guarda lo que él escribió.

Una expresión matemática es un árbol, no una cadena. El módulo nucleo/sintaxis/ la analiza por precedencia —lexer, parser tipo Pratt, extractor de rasgos y revisor— y produce dos cosas que conviene no mezclar: rasgos estructurales que alimentan al emparejador, y un aviso para el alumno que sólo se emite cuando merece la pena.

Los rasgos predicen qué hechos harán falta

La relación entre sintaxis y semántica se puede medir aquí sin metáforas, porque están las dos mitades: el enunciado en Lean es un objeto puramente simbólico, y los lemas que su prueba usó son lo que hizo falta en el universo matemático. Sobre 22 117 pares y los 100 lemas con suficientes ejemplos:

Sesenta y ocho rasgos igualan a cuarenta mil, y juntos suman cuatro puntos: no son la misma información. Y lo que aprende la estructura se puede leer, que es lo que una bolsa de n-gramas no da nunca:

El sistema y Lean hacen búsquedas distintas, y durante mucho tiempo compitieron sin saberlo. La diferencia no es de calidad: es de tipo de entrada. Eso parte el trabajo en dos mitades con dueños distintos, y la frontera es el momento en que existe un enunciado formal.

La evidencia del reparto

Antes de formalizar, con la consulta todavía en prosa, buscar sobre el índice completo no supera al azar; el vocabulario curado lo bate trece veces:

Después de formalizar, con un objetivo formal delante, la búsqueda del grafo pierde por dos órdenes de magnitud:

Las cinco capas

                consulta (ES/EN)
                       │
  L0  LENGUA       palabras clave ES/EN → concepto      ANTES
  L1  CONCEPTO     189 curados · vocabulario #check       DE
  L2  TERRITORIO   147 generados · dónde vive        FORMALIZAR
                       │
             ENUNCIADO FORMAL   ←── la frontera
                       │
                  LEAN VERIFICA
                       │
  L3  EVIDENCIA    forma del objetivo → qué cierra     DESPUÉS
  L4  EMERGENCIA   colímites sobre teoremas aceptados
                       │
                  LA RESPUESTA   veredicto delante del texto

Qué está cableado hoy

L0 — Lengua

Por qué. Es lo único que Lean no puede hacer: leer una frase. Un índice de 217 419 nombres formales no contiene la correspondencia «grupo → Group, Subgroup, MonoidHom»; ésa la escribió una persona.
Qué muestra. 62,1 % de acierto de área equilibrado, frente al 33,3 % de responder siempre la clase mayoritaria.

L1 — Concepto

Por qué. El modelo inventa 21 de cada 28 identificadores cuando tira de memoria.
Qué muestra. 180 de 186 nombres existen; los seis restantes son espacios de nombres y están filtrados antes del prompt, así que la etiqueta «verificado» es cierta para todo lo que se ofrece.
Lo que NO muestra: que eso haga verificar más a Lean. Se midió — rescata 3, rompe 2, p = 1,0. Es puntería, no resultado.

L2 — Territorio

Por qué. El curado nombra 189 conceptos; la taxonomía de Mathlib tiene 1 139. Los generados dan alcance para reconocer temas.
Qué muestra. Que su vocabulario no transfiere, por tres vías medidas: sin criba 17,45 %, criba por uso 20,77 % y cuota separada 20,18 %, frente al 21,64 % de la base. El módulo de un objeto generado es un rincón de su área, no su centro.

L3 — Evidencia

Por qué. Pasada la frontera la pregunta ya no es «de qué trata» sino «qué cierra esto», y eso lo decide la forma del objetivo. Cada intento fallido cuesta una compilación de 12 a 30 segundos.
Qué hace. Un clasificador ordena la cascada combinando n-gramas —que ven los símbolos— con 74 rasgos estructurales, que ven la forma. No son redundantes: 60,53 % y 61,14 % por separado, 67,11 % juntos, sobre un nulo de 23,77 % —responder siempre nlinarith—.
Qué muestra. Medido con el modelo de producción contra el orden fijo real, sobre 1 530 casos que no vio:

3,7 veces menos invocaciones de Lean que el orden fijo, y bate al nulo fuerte por 0,87 posiciones. Es la pieza que más mejora la búsqueda de todo el sistema.

L4 — Emergencia

Por qué. El paisaje de CR_org, de donde salen los patrones que se ligan en colímites, se alimentaba de lo que el emparejador léxico adivinaba: el grafo llevaba la cuenta de sus propias conjeturas.
Qué hace. Dos conceptos coocurren si un teorema que Lean aceptó habla de los dos — 40 025 teoremas de Mathlib, corregido por frecuencia.
Qué muestra. Que los pares que emergen son relaciones genuinas, medidas por el exceso sobre lo esperado:

Qué parte busca y qué parte explica

Las capas no hacen todas lo mismo, y confundirlo lleva a pedirle a una lo que sólo puede dar otra.

La pieza que más mejora la búsqueda no es el grafo de conceptos: es L3, el rankeador del estado de prueba, que trabaja del lado formal de la frontera. L1 busca bien y no llega al resultado. Y L4 no busca nada y es de lo más valioso para explicar: no entra en el prompt ni ordena tácticas; lo que aporta es poder decirle a un alumno que group-theory y subgroups-cosets aparecen juntos en 206 teoremas que Lean aceptó, veinte veces más de lo que cabría esperar por azar (exceso +4,32).

Hay dos almacenes con trabajos distintos, y se miden distinto. Uno dice de qué habla algo; el otro dice qué es cierto.

Por qué hacen falta las dos

De los 169 nombres que el grafo inyecta hoy, 3 son teoremas o lemas y 166 son tipos, estructuras y clases: el grafo aporta los sustantivos. Y ahí no es donde el modelo falla. De 28 nombres que el modelo propuso de memoria, los 21 inexistentes eran todos lemas — tsum_geometric_two, Subgroup.isCyclic, isOpen_union: siguen la convención de nombres al dedillo y no existen.

El modelo acierta razonablemente los sustantivos e inventa los hechos. La lista existe para cubrir esa mitad, y el índice de nombres (§9) para desmentir la otra.

Una categoría finita: 353 objetos y 1 586 morfismos, con identidad en cada objeto y composición por transitividad. Cada nodo lleva un sort que dice qué clase de objeto es, y ese tipado lo hace cumplir el constructor: una dependencia mal tipada se rechaza.

Un solo grafo, cosido por el anidamiento de módulos

Los nodos generados (125) y los curados (173) están cosidos por la jerarquía que Mathlib ya tiene escrita en el anidamiento de sus módulos, que va de lo general a lo especial — la misma dirección que el grafo curado sigue con group-theory → ring-theory → field-theory. Un cuerpo es un anillo con más axiomas: la teoría general se inyecta en la especializada.

aristas que cruzan curado ↔ generado    125
generados con ancestro curado común    109 de 125
nodos que alcanza la lógica            278 de 320

Lo que el esqueleto de módulos no da: los generados y los curados son hermanos bajo un área, no descendientes, porque la profundidad del módulo no ordena la generalidad — LinearAlgebra.Basis está a profundidad 2 y LinearAlgebra.Matrix.Defs a 3, y sin embargo el álgebra lineal es más general que la noción de base. Eso requiere un juicio que Mathlib no contiene.

Los ciclos son de la agregación, no de la matemática

Hay 134 ciclos, todos entre nodos generados; entre los 173 curados hay cero. El DAG oficial de imports es acíclico —Lean prohíbe imports circulares— pero al colapsar 7 747 módulos en conceptos de dos niveles aparecen:

Topology.Instances → Analysis.Asymptotics → Analysis.Complex → Topology.Instances

Son tres desarrollos distintos: los espacios vectoriales topológicos necesitan la topología de ℝ≥0∞, el análisis asintótico complejo necesita la notación Θ, y la topología de ℂ necesita su estructura normada. Nadie dio la vuelta. El ciclo marca dónde la división en ramas deja de funcionar, no un recorrido.

El grafo tiene dos preguntas distintas sobre cada nodo, y separarlas es lo que le da estructura: area dice de qué rama habla —y es la base— y sort dice qué clase de objeto es —y determina la fibra—.

El claim que el sistema sostiene, y con esa precisión: I es el colímite de P en la subcategoría delgada finita G_n — no en una categoría arbitraria. La propiedad universal, la unicidad del mediador y el puente con CategoryTheory.Limits.IsColimit de Mathlib están demostrados, y el Python que los implementa está auditado contra ellos (§13).

Dos cosas distintas que Lean comprueba aquí

Los archivos de CategoryFoundations/ demuestran los teoremas generales: que ser colímite equivale a ser join en un preorden delgado, que el mediador es único, que la construcción encaja con IsColimit de Mathlib. Son enunciados sobre cualquier grafo, y se prueban una vez.

Lo que no dicen es si este nodo concreto es colímite de este patrón en el grafo de hoy. Eso es una afirmación sobre una instancia finita, y es decidible: hay 353 objetos, así que el ∀ del enunciado se recorre entero. build_colimit(…, con_lean=True) genera ese enunciado en Lean —sin import Mathlib, para que compile en segundos— y lo cierra con decide, que lo comprueba el kernel y no el compilador. El veredicto queda en Colimit.lean_verified.

Al enunciado sólo viajan los morfismos que consulta —los que salen del diagrama y los que salen del ápice—, que no es una poda sino el conjunto exacto que la propiedad mira; el universo del cuantificador sigue siendo los 353 nodos. Sin ese recorte, los casos verdaderos agotaban el presupuesto del kernel a los 25 segundos.

Tres estructuras derivadas del fuente de Mathlib, con trabajos distintos: una dice qué es cierto, otra qué nombres existen, y la tercera qué herramienta puede usar cada lema.

Mathlib no etiqueta por rama — etiqueta por táctica

Se buscó una anotación de área y no existe. Lo que sí hay, en 83 111 líneas y 162 atributos distintos, es qué herramienta puede usar cada lema:

@[simp]        40 736      @[gcongr]       575      @[continuity]  255
@[norm_cast]    2 257      @[grind]        547      @[mono]        244
@[fun_prop]     1 796      @[aesop]        286      @[measurability]

Es un índice herramienta → lemas curado por los mantenedores, y sirve para algo concreto: el 42,1 % de las premisas que citan las pruebas ya llevan @[simp], y simp las conoce sin que nadie se las pase. Filtrarlas movió la selección de premisas de empatar con un prior de frecuencia (9,4 % contra 9,2 %) a superarlo: 14,0 % contra 11,7 %.

Cobertura de la taxonomía

Los conceptos de nivel 2 que el grafo cubre alcanzan 137 476 de los 173 636 teoremas de Mathlib (79,2 %) con 211 conceptos de 1 139. La cobertura es muy desigual por rama —Álgebra 25 410 de 27 560, Análisis 20 178 de 21 240, Geometría algebraica 1 643 de 2 906, y Condensed 0 de 75—, y esa desigualdad es informativa: marca dónde el grafo curado tiene huecos reales.

Hay dos cosas que conviene no mezclar. Lo que Lean dice abre cuatro caminos, y tres de ellos siguen trabajando. El veredicto viene después, y no coincide con «compiló».

El árbol de veredicto, en el orden exacto en que se decide

Cuando Lean acepta la estructura pero queda un sorry, entran doce tácticas con su tiempo límite. El orden lo propone el grafo a partir de la forma del objetivo.

Desde el paso 2 del lazo (§18) el bloque ya no se compila como fichero en el camino servido: se elabora en la sesión viva de Lean, con el mismo orden y el mismo texto, y el fichero sólo confirma la táctica ganadora. Lo que sigue describe el bloque, que es el mismo en las dos vías.

rfl 1s   simp 2s   norm_num 2s   ring 2s   ring_nf 3s   field_simp 3s
linarith 3s   nlinarith 4s   omega 3s   exact? 5s   apply? 5s   aesop 8s

orden                 posición media   1er intento   en los 3
regla de hoy                1,26          88,4 %       94,4 %
MODELO NULO                 1,09          94,4 %       99,4 %
clasificador entrenado      1,06          95,9 %       99,4 %

Una tabla de mediciones con filas que dicen «no bate al nulo» no sirve de nada si esas capacidades siguen ejecutándose. nucleo/decisor.py convierte la evidencia en control de flujo.

El catálogo tiene trece capacidades. Ante una consulta matemática con Lean disponible corren siete; 0 están apagadas porque no baten a su nulo; una bate al suyo y no está cableada, y el decisor dice por qué en cada caso; dos dependen de la consulta, porque su guarda sólo aplica a algunas; y tres no tienen medición contra un nulo —entre ellas lazo_por_pasos, el paso 3 del lazo (§18), cuya puerta con modelo no se ha corrido—.

Que ninguna capacidad esté hoy apagada por medición no es que la regla se haya relajado: las diez que no batieron a su nulo se quitaron del código el 21 de septiembre de 2026. Un candidato evaluado y descartado es información, así que no desaparece: queda en data/descartado.json —qué hacía, su cifra, su nulo y el commit donde se puede leer entero— y en §16.

Las construcciones categóricas del núcleo no se implementan primero en Python y se justifican después: se demuestran en Lean, y el Python se audita contra los teoremas. El corpus son 387 teoremas y lemas en 22 archivos, sin un solo sorry — y eso se comprueba preguntándole al compilador con #print axioms, no con grep: ninguna constante depende de sorryAx.

Todo lo que se afirma de este sistema se afirma con una medición detrás, y toda medición cumple cuatro condiciones. No son formalidades: cada una corresponde a una forma concreta de producir una cifra creíble y falsa.

El bucle que no cuesta dinero

La formalización es el único paso que necesita el modelo. Con METAMAT_GRABAR=1 se graba el código del modelo antes de que Lean lo vea, y todo lo que el sistema hace después —reparación de imports, cascada, premisas, veredicto— se reejecuta con Lean de juez y coste cero.

La frontera está donde tiene que estar, y hay un test que lo impide mover: si el gancho de grabación se colocara detrás de la normalización, la reejecución mediría el sistema contra su propia salida y daría siempre lo mismo.

El resultado que ordena a los demás: ¿aporta el sistema?

Durante mucho tiempo la comparación fue «el sistema con el grafo» contra «el sistema sin el grafo». Esa pareja contesta si aporta el grafo, no si aporta el sistema: la rama sin grafo sigue llevando reparación, premisas, cascada y ejemplos. Faltaba el suelo — el mismo modelo, una llamada, sin nada.

Catorce mediciones, cada una con su modelo nulo. La figura las pone todas en la misma escala —cuántas veces bate a su nulo— para que se puedan comparar componentes que miden cosas distintas.

El banco de fidelidad

Es el instrumento que responde a la pregunta central: ¿el teorema que Lean verifica es el que se preguntó? Verificar fielmente algo falso es tan malo como verificar infielmente algo cierto, así que un caso sólo cuenta como bueno si salen bien las tres cosas:

1. Verificación — qué dijo Lean.
2. Fidelidad — un juez independiente decide si el enunciado formalizado es el de la pregunta, sin ver el veredicto de Lean, para que el sello no lo contamine.
3. Honestidad — para los enunciados falsos a propósito, el sistema debe rechazarlos o probar su negación, y la respuesta debe abrir diciéndolo.

El banco tiene 24 casos en tres grupos: 16 ciertos y formalizables, 4 falsos a propósito y 4 controles que no son matemáticas y no deberían tocar Lean. La corrida rápida es una muestra estratificada de ocho —4/2/2— para que la parte que discrimina siga estando representada.

Costaron el mismo trabajo que los positivos y valen igual. Están aquí para que nadie los repita, y porque un sistema que sólo publica lo que funciona no se puede evaluar.

La red neuronal aprendió una constante

Un encoder de premisas entrenado para Lean tampoco entra

1 312 tests en 67 suites, verdes en los dos intérpretes con los que se trabaja. Los que más valen no comprueban que el código funcione: comprueban que el sistema no pueda volver a afirmar más de lo que sabe.

Las tres vueltas de §1 son un lazo por intentos: el modelo escribe la prueba entera, Lean compila el fichero, y si falla el modelo recibe los errores y la reescribe entera. Lo que se está construyendo es un lazo por pasos: el modelo propone una táctica sobre un estado de prueba, Lean la evalúa, y lo que contesta —el estado nuevo, o por qué falló— condiciona el paso siguiente. Es la categoría de estados de §8 hecha viva: cada flecha la crea Lean en línea, no un corpus.

Se construye en cinco pasos, y cada uno termina en una medición que decide si se sigue. Ninguno entra en el camino servido por estar construido: entra si su capacidad bate a su nulo en el decisor (§12).

Paso 1 · una sesión de Lean que no se apaga

Hoy cada comprobación arranca Lean y vuelve a cargar la cabecera: el coste está ahí, no en la táctica. La sesión es un proceso de Lean —el repl de leanprover-community, con el mismo toolchain que el proyecto— que carga la cabecera una vez y después recibe tácticas sobre estados. Con la cabecera estrecha del camino servido, medido en esta máquina:

Paso 2 · la cascada, en la sesión

Cuando queda un sorry, la cascada de §11 prueba doce tácticas en un first |. Hoy eso es un compilado por sorry, cierre o no. En el paso 2 el mismo bloque, con el mismo orden y sobre el mismo texto, se elabora en la sesión viva; si cierra, el fichero confirma la prueba con la táctica ganadora. Medido sobre 30 casos, las dos vías:

Es lo que se predijo antes de medir: empate en cierres y la ganancia en los fallos, que son la mayoría —la sesión no necesita compilar para saber que no cerró—. La fila con cabeceras apenas gana porque en este banco cada teorema trae la cabecera de su fichero; en el sistema servido la cabecera estrecha es casi siempre la misma y se paga una vez por proceso. El decisor lee esa fila, la peor para la sesión, y la enciende; si una medición futura pierde un solo cierre, la cifra desaparece del fichero y la apaga sola.

El modo importa. La primera versión aplicaba el bloque como táctica sobre el estado, y el repl no aplica ahí el límite de heartbeats: en un objetivo duro se agotaba a los 120 s. Se elabora como comando, con su límite, igual que un fichero pero sin arrancar Lean. El modo táctica queda para el paso 3, que tendrá que resolver ese límite.

Paso 3 · el mediador, construido y todavía sin su puerta

nucleo/lazo/ hace la búsqueda de la propuesta: cada sorry es una raíz, los proponentes sugieren tácticas —D0, la cascada, una a una; D3, el modelo, con la retroalimentación del estado—, la sesión evalúa cada una, y el fichero verifica la prueba ensamblada. Los estados se identifican normalizados, cada uno guarda sus fallos para el paso siguiente, y todo intento va a data/transiciones_vivas.jsonl: las alternativas que la categoría de estados construida desde LeanWorkbook no tenía.

Su puerta gasta modelo y no se ha corrido, así que el decisor lo tiene apagado. Lo que sí está medido, gratis, es un suelo: las dos ramas sobre las mismas 20 formalizaciones grabadas, A el camino servido de hoy sobre el código que escribió el modelo, B el lazo sin modelo —sólo D0— sobre su enunciado.

El caso que sólo el lazo cierra es «todo subgrupo de un grupo cíclico es cíclico»: el modelo escribió la prueba con un lema que no existe, y el lazo la cerró con exact?, que busca por el tipo sobre toda la biblioteca. Es la frontera de §5 en un solo caso. Con 20 consultas no significa nada estadísticamente, y A no incluye las rondas de reparación, que gastan modelo.

Paso 4 · de dónde salen las tácticas

La cascada propone nombres: «prueba nlinarith». Lo que cierra una desigualdad de competición casi nunca es el nombre desnudo, sino nlinarith [sq_nonneg (a - b), …], con los hechos que hay que citarle. Esos argumentos están escritos en las transiciones de LeanWorkbook de §8: los vecinos de estado buscan el estado más parecido y copian lo que lo cerró. La otra fuente es D2: apply? lanzado como sonda para leer sus «Try this». Todo se mide sin modelo, con el índice construido sólo con la partición de entrenamiento.

Como sustitutos del rankeador, los vecinos no ganan: 76 frente a 79. Pero son complementarios —22 estados que sólo cierran ellos, 25 que sólo cierra el rankeador—, y la prueba que decide es otra: como fuente añadida del lazo, con los mismos 60 estados y el mismo presupuesto:

Los vecinos entran como fuente del lazo: rescatan sin romper, y además gastan menos Lean, porque cierran antes. D2 no entra —y su código se quitó—: no rescata ninguno y sus sondas se comen el presupuesto; con las tres fuentes juntas se pierden casos que D0 + vecinos cerraba. Las dos decisiones las tiene escritas el decisor, que lee estos ficheros. Y ninguna llega al alumno todavía: viven dentro del lazo, que sigue sin su puerta con modelo.

La tercera fuente es el índice denso: un codificador entrenado para Lean —premise-selection, Zhu et al., ICLR 2026— que acerca el estado impreso a las premisas de Mathlib que su prueba usó. Las 382 212 premisas vienen ya codificadas; cada una se prueba como exact, apply y rw, y todas juntas en simp […]. Mismo banco, mismos 60 estados, y la regla escrita antes: entra si bate a D0, y se queda junto a los vecinos sólo si les añade algo.

El denso no entra, y su código se quitó. En ninguno de los caminos verificados aparece una táctica suya; su único «rescate» lo cerró exact?, que es de D0, en un caso en que el brazo D0 se había colgado en una sola llamada. Lo que sí hace es gastar: trece plantillas por estado que Lean rechaza y que agotan el presupuesto antes de que lleguen las que cierran. La corrida repite a los vecinos —48 otra vez—; D0 dio 40 donde el paso 4 dio 41, y ésa es la escala del ruido de un presupuesto en segundos.

El sesgo de los vecinos queda dicho: LeanWorkbook es matemática de competición, y fuera de desigualdades y álgebra elemental propondrán tácticas que Lean rechazará en centésimas. Los dos codificadores de 7 000 millones de parámetros de la propuesta —LeanSearch-PS y Lean Finder— están descargados, pero con 4,3 GB de GPU no codifican Mathlib a una velocidad útil: no están medidos.

Paso 5 · φ, de qué conceptos habla un estado

φ lleva cada estado de prueba a los conceptos del grafo cuyos nombres verificados de Mathlib aparecen en él, por coincidencia exacta —la regla que hizo fiable a L4—. No es un funtor y no se usa para buscar: sirve para que la explicación diga «este paso pasó de hablar de subgrupos a hablar de órdenes». La propuesta predecía que leerlo del texto impreso pierde casi todo, porque Lean escribe ℝ y ∑ y no Real ni Finset.sum; la otra lectura pide a Lean las constantes que el estado usa, con una táctica propia. Sobre 168 estados raíz —las consultas de la campaña y LeanWorkbook—:

La cobertura de las constantes es hueca. 145 de los 150 estados de LeanWorkbook sólo recibían la etiqueta del tipo donde viven los números —ℝ daba «análisis real», ℕ «teoría elemental de números»—, y una etiqueta que sale en todo no explica nada. Quitados los tipos portadores, las dos lecturas empatan: 21 contra 21. La predicción de la propuesta no se confirma: quitada la notación, lo que queda apunta a otro límite —que el grafo nombre las constantes que estos estados usan—, y eso no está medido.

Lo que construirlo destapó del sistema de antes

• La cascada servida no cerraba nada desde el 2026-09-04. field_simp no existe bajo la cabecera estrecha, y un first | es una sola pieza de sintaxis: si una táctica no existe, Lean rechaza el bloque entero sin probar ninguna. Ni a + b = b + a. Los tests usaban un Lean de mentira y no podían verlo; ahora la cabecera trae FieldSimp y hay un test que compila de verdad. La campaña del lazo por intentos (2026-09-10) se midió con ese fallo; de las 63 formalizaciones grabadas, sólo 2 tenían un sorry, que es donde entra la cascada.
• apply? dejaba muerto lo que iba detrás. Cuando no encuentra prueba, cierra el objetivo con sorry: dentro del first es una rama que no falla, y las tácticas posteriores no se probaban. El fichero no daba sello falso; ahora va siempre la última. No hay un caso medido en que eso costara un cierre.
• import Mathlib no tarda 742 s. La cifra estaba en diez sitios sin procedencia, justificando la cabecera estrecha porque «siempre expira». Medido de nuevo: 24 s entera y 11 s estrecha, las dos muy por debajo del límite de 360 s. La cabecera estrecha se queda, por coste.

Lo que el sistema no hace

• No demuestra teoremas por sí solo. Formaliza y verifica. La prueba la escribe el modelo o la cierra la cascada de tácticas.
• El grafo no decide qué es cierto en ningún punto. Eso es Lean, siempre.
• Sin API no hay formalización, ni chat, ni banco de fidelidad. Lo que sigue vivo sin ella es todo el trabajo de validar y mejorar el núcleo, que es la mayor parte de este documento.

Preguntas abiertas

• El banco de fidelidad completo, los 24 casos con juez ciego. Es la única medida de si la respuesta responde a la pregunta, y la única que sigue necesitando presupuesto de modelo.
• Un banco en español con premisas de oro. Sin él, todo lo que se construye para el alumno hispanohablante se mide en inglés y por analogía.
• Subir el n de la campaña. Los tres contrastes pareados corren sobre 20 casos (15 en la rama sin reparación). Con ese tamaño, «rescata 4 y rompe 0» no llega a significancia aunque el efecto sea real.

Identificado, con el camino claro

• La categoría de estados existe, y lo que le falta no son datos. Estaba aquí como «las tácticas deberían ser flechas» y ya está construida (nucleo/graph/estados.py): 24 752 estados, 25 206 tácticas, no goals terminal, el 46,4 % de las flechas componen. Lo que no puede dar es la parte que hacía falta: sólo 72 de los 24 752 estados registran dos tácticas distintas, porque el corpus recoge la prueba que alguien escribió y no las que descartó. Aprender a elegir exige generar esas alternativas probando tácticas contra estados reales. Eso ya no cuesta un compilado por intento: con la sesión viva una táctica cuesta centésimas de segundo (§18). Es el paso 3.
• La base no es un orden, y por eso no hay viaje general. Esto decía que faltaban morfismos que crucen de área y que eran «lo único que puede convertir el funtor en una fibración». Es falso, y lo refuta el propio repositorio: la clausura transitiva es monótona, así que una arista nueva sólo puede añadir relaciones a la base, y las áreas ya forman una componente fuertemente conexa de 21 de 23. Añadir morfismos que crucen empeora la tasa — medido en scripts/base_no_es_un_orden.py. Los 105 de 688 que cruzan hoy generan 462 relaciones entre áreas al cerrar: la base afirma de más. La palanca no son los morfismos sino la asignación de áreas. Lo que sí se puede usar son los 105 levantamientos que existen uno a uno (data/viajes.json), al 7,3 % de lo que la base promete y sólo 1,1× sobre el azar.
• La fibra de hechos. data/banco_lemas.jsonl son 23 243 pares (enunciado, lemas que la prueba usó): un grafo bipartito esperando a ser construido, que hoy sólo alimenta un índice plano.
• Un índice de sustantivos consultado por la consulta, como premisas.py hace con los lemas. La lista está construida y verificada; lo que no funciona es la clave «módulo del nodo».
• No hay lematización en el emparejador, así que primos no casa con primo. Añadirla mueve la precisión y necesita su propia medición.
• Seis dependencias del grafo siguen bajo sospecha de ir en sentido contrario, según la comparación con el DAG oficial.