Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge

Resumen Técnico: Hacia una capa de puente entre el conocimiento bibliográfico y el conocimiento matemático formalizado

Planteamiento del problema
El conocimiento matemático moderno se encuentra actualmente fragmentado en dos infraestructuras estructuralmente independientes. Por un lado, las bases de datos bibliográficas como MathSciNet y zbMATH Open indexan el registro de investigación legible por humanos, capturando metadatos de publicación, redes de citación y revisiones de expertos. Por otro lado, las bibliotecas de pruebas formales (por ejemplo, la mathlib de Lean) y los probadores de teoremas interactivos (ITPs) codifican la matemática verificable por máquinas como objetos formalmente comprobados. Aunque estos ecosistemas son complementarios, permanecen desconectados: los sistemas bibliográficos no indican si los resultados han sido formalizados, y las bibliotecas formales se organizan en torno a grafos de dependencia internos en lugar de metadatos de publicación. Aunque existen "artefactos de alineación" (como artículos de revisión o documentación) que mapean resultados clásicos con desarrollos mecanizados, estos mapeos están fragmentados, no están estandarizados y no se integran sistemáticamente en una capa consultable.

Metodología
El artículo propone una base de datos de puente relacional diseñada para integrar estas infraestructuras existentes sin reemplazarlas. La metodología central consta de tres componentes:

1. Integración Arquitectónica: El sistema actúa como una infraestructura de alineación que vincula registros bibliográficos (de MathSciNet y zbMATH Open) con artefactos formales (de Lean, Reservoir, etc.). No realiza una nueva revisión por pares ni verificación formal, sino que sirve como una plataforma de archivo que registra las correspondencias entre publicaciones y código formal.
2. Puntuación de Formalización ($S(P_i)$): Los autores definen una métrica cuantitativa para medir el grado de formalización de un artículo específico $P_i$.
   • El artículo es tratado como una colección de enunciados matemáticos $S_i$ (definiciones, lemas, teoremas, conjeturas, etc.).
   • Se asigna un indicador binario $\phi(s)$ a cada enunciado $s$: 1 si está totalmente formalizado en Lean, 0 en caso contrario.
   • Distinción en los requisitos:
     • Enunciados puros (definiciones, construcciones, conjeturas) requieren únicamente la existencia del objeto formal.
     • Enunciados probados (teoremas, lemas) requieren tanto el enunciado formal como una prueba formal completa.
   • La puntuación se calcula como: $S(P_i) = 100 \cdot \frac{\sum_{s \in S_i} \phi(s)}{|S_i|}$.
3. Estudio de viabilidad mediante la alineación de documentos cruzados: Para demostrar que estas puntuaciones pueden estimarse a escala, los autores utilizaron Modelos de Lenguaje de Gran Escala (LLMs) en un entorno de zero-shot. Se instruyó al modelo para comparar un artículo matemático informal (PDF 1) contra un documento de formalización o implementación en Lean (PDF 2). El modelo recibió instrucciones para:
   • Extraer enunciados matemáticos granulares del texto informal.
   • Clasificarlos como "Puros" o "Probados".
   • Identificar correspondencias semánticas en el texto formal.
   • Calcular la puntuación de formalización basada en la ratio de enunciados coincidentes.

Contribuciones clave

• Capa de interoperabilidad: Una propuesta de base de datos que unifica los registros bibliográficos con los entornos de verificación formal, vinculando los metadatos de publicación con los repositorios de código formal.
• Definición de la Puntuación de Formalización: Una métrica rigurosa a nivel de artículo ($S(P_i)$) que cuantifica la cobertura de una publicación dentro de los sistemas formales, distinguiendo entre la existencia de definiciones y la presencia de pruebas.
• Demostración de viabilidad: Un estudio de prueba de concepto que muestra que los LLMs pueden estimar con éxito estas puntuaciones mediante la alineación de textos informales con artefactos formales, permitiendo un análisis a gran escala de la cobertura de formalización.

Resultados experimentales
Los autores realizaron experimentos con seis artículos matemáticos utilizando Google Gemini sin ajuste fino (fine-tuning). Los resultados demostraron la capacidad del sistema para distinguir entre distintos grados de formalización:

• Alta cobertura: El problema del empaquetamiento de esferas en la dimensión 8 recibió una puntuación de 100, indicando una formalización completa.
• Cobertura parcial: Artículos sobre la irracionalidad de $\zeta(3)$ y esquemas Proj multigraduados recibieron puntuaciones de 50 y 67.74 (y 96.30 en un segundo experimento), reflejando una formalización sustancial pero incompleta.
• Baja/Sin cobertura: Un artículo sobre "Dilataciones de categorías" recibió 41.67, y un estudio sobre "Magnetismo algebraico" (que no tenía implementación en Lean) recibió 0 al ser contrastado con documentación no relacionada.
  Los experimentos confirmaron que el modelo podía identificar correctamente cuando no existía formalización relevante y podía diferenciar entre trabajos totalmente y parcialmente formalizados.

Significado y pretensiones
El artículo posiciona este trabajo como un primer paso hacia la integración de los ecosistemas bibliográficos y matemáticos formales en grafos de conocimiento escalables y accionables por máquinas. Los autores declaran explícamente que el sistema propuesto no es un reemplazo de las infraestructuras de publicación o verificación existentes. En su lugar, sirve como una "capa conectiva" que sistematiza el conocimiento de alineación informal existente en un recurso estructurado y consultable.

La importancia radica en la capacidad de:

1. Proporcionar acceso unificado a los resultados publicados y sus contrapartes formales.
2. Permitir el análisis a gran escala de qué parte de la literatura matemática ha sido formalizada.
3. Crear una base para vincular publicaciones con objetos de prueba formal, apoyando potencialmente futuros flujos de trabajo de matemáticas generadas por IA y de colaboración híbrida humano-IA.

Los autores reconocen las limitaciones, señalando que el procesamiento de PDFs introduce ambigüedad, la calidad de la recuperación afecta la precisión de la puntuación y los LLMs pueden producir correspondencias espurias. En consecuencia, presentan el sistema como un "marco de mejor esfuerzo" (best-effort framework) para la alineación relacional en lugar de un mapeo perfectamente fiel, con la expectativa de que los hipervínculos y los mapeos sean eventualmente curados manualmente o mediante procesos supervisados similares a las prácticas bibliográficas actuales.