Cinco capas alrededor de una frontera: dónde termina la palabra y empieza el tipo

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:

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 es inerte en el 3. Resumirlo en una sola cifra sería mentir por agregación.

Conviene separar dos cosas que el paso 5 mezcló mucho tiempo: la regla por área que proponía el grafo de conceptos no batía a su nulo (1,26 frente a 1,09) y está apagada por el decisor; 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     158 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. 58,7 % 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 190 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: 321 objetos y 1 349 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 321 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 352 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.

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 doce capacidades. Ocho tienen evidencia y guarda, tres están apagadas por medición, una —el emparejador semántico— nunca llegó a producción y se conserva en el catálogo a propósito: un candidato evaluado y descartado es información, y borrarlo invita a reinventarlo.

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.

1 085 tests en 53 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.

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

• Las tácticas deberían ser flechas, no nodos. Hoy son 9 sumideros que reciben 453 aristas. Sus objetos deben ser estados de prueba y sus morfismos las tácticas. Hay 25 214 transiciones state_before → tactic → state_after en disco para construir esa categoría y medirla sin API, y la cascada en un compilado hace que explorarlo ya no cueste tres minutos por consulta.
• Faltan morfismos que crucen de área. Es lo único que puede convertir el funtor verificado en una fibración: hoy sólo 29 de 230 morfismos de orden cruzan. No falta formalización — la definición y sus propiedades están demostradas sin sorry—, faltan datos.
• 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.