Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge

Resumo Técnico: Rumo a uma Camada de Ponte entre o Conhecimento Bibliográfico e o Conhecimento Matemático Formalizado

Definição do Problema
O conhecimento matemático moderno encontra-se atualmente fragmentado em duas infraestruturas estruturalmente independentes. De um lado, bases de dados bibliográficas como MathSciNet e zbMATH Open indexam o registro de pesquisa legível por humanos, capturando metadados de publicação, redes de citações e revisões de especialistas. Do outro lado, bibliotecas de provas formais (ex: mathlib do Lean) e provadores de teoremas interativos (ITPs) codificam a matemática verificável por máquinas como objetos formalmente checados. Embora esses ecossistemas sejam complementares, eles permanecem desconectados: sistemas bibliográficos não indicam se os resultados foram formalizados, e as bibliotecas formais são organizadas em torno de grafos de dependência internos, em vez de metadados de publicação. Embora existam "artefatos de alinhamento" (como artigos de revisão ou documentação) que mapeiam resultados clássicos para desenvolvimentos mecanizados, esses mapeamentos são fragmentados, não padronizados e não são sistematicamente integrados em uma camada consultável.

Metodologia
O artigo propõe um banco de dados de ponte relacional projetado para integrar essas infraestruturas existentes sem substituí-las. A metodologia central envolve três componentes:

1. Integração Arquitetural: O sistema atua como uma infraestrutura de alinhamento que vincula registros bibliográficos (de MathSciNet e zbMATH Open) com artefatos formais (de Lean, Reservoir, etc.). Ele não realiza nova revisão por pares ou verificação formal, mas serve como uma plataforma de arquivamento que registra correspondências entre publicações e código formal.
2. Pontuação de Formalização ($S(P_i)$): Os autores definem uma métrica quantitativa para medir a extensão da formalização de um artigo específico $P_i$.
   • O artigo é tratado como uma coleção de enunciados matemáticos $S_i$ (definições, lemas, teoremas, conjecturas, etc.).
   • Um indicador binário $\phi(s)$ é atribuído a cada enunciado $s$: 1 se totalmente formalizado em Lean, 0 caso contrário.
   • Distinção nos Requisitos:
     • Enunciados puros (definições, construções, conjecturas) requerem apenas a existência do objeto formal.
     • Enunciados provados (teoremas, lemas) requerem tanto o enunciado formal quanto uma prova formal completa.
   • A pontuação é calculada como: $S(P_i) = 100 \cdot \frac{\sum_{s \in S_i} \phi(s)}{|S_i|}$.
3. Estudo de Viabilidade via Alinhamento entre Documentos: Para demonstrar que essas pontuações podem ser estimadas em escala, os autores utilizaram Modelos de Linguagem de Grande Escala (LLMs) em um cenário zero-shot. O modelo foi incumbido de comparar um artigo matemático informal (PDF 1) contra um documento de formalização ou implementação em Lean (PDF 2). O modelo foi instruído a:
   • Extrair enunciados matemáticos granulares do texto informal.
   • Classificá-los como "Puros" ou "Provados".
   • Identificar correspondências semânticas no texto formal.
   • Calcular a pontuação de formalização baseada na razão de enunciados correspondentes.

Principais Contribuições

• Camada de Interoperabilidade: Uma proposta de banco de dados que unifica registros bibliográficos com ambientes de verificação formal, vinculando metadados de publicação a repositórios de código formal.
• Definição de Pontuação de Formalização: Uma métrica rigorosa, ao nível do artigo ($S(P_i)$), que quantifica a cobertura de uma publicação dentro de sistemas formais, distinguindo entre a existência de definições e a presença de provas.
• Demonstração de Viabilidade: Um estudo de prova de conceito mostrando que LLMs podem estimar essas pontuações com sucesso ao alinhar textos informais com artefatos formais, permitindo uma análise em larga escala da cobertura de formalização.

Resultados Experimentais
Os autores conduziram experimentos em seis artigos matemáticos usando o Google Gemini sem ajuste fino (fine-tuning). Os resultados demonstraram a capacidade do sistema em distinguir entre diferentes graus de formalização:

• Alta Cobertura: O problema de empacotamento de esferas na dimensão 8 recebeu uma pontuação de 100, indicando formalização total.
• Cobertura Parcial: Artigos sobre a irracionalidade de $\zeta(3)$ e esquemas Proj multigradados receberam pontuações de 50 e 67,74 (e 96,30 em um segundo experimento), refletindo uma formalização substancial, porém incompleta.
• Baixa/Nenhuma Cobertura: Um artigo sobre "Dilatações de categorias" recebeu 41,67, e um levantamento sobre "Magnetismo algébrico" (que não possuía implementação em Lean) recebeu 0 quando confrontado com documentação não relacionada.
• Os experimentos confirmaram que o modelo poderia identificar corretamente quando nenhuma formalização relevante existia e poderia diferenciar entre obras totalmente e parcialmente formalizadas.

Significância e Alegações
O artigo posiciona este trabalho como um primeiro passo para integrar os ecossistemas bibliográfico e matemático formal em grafos de conhecimento escaláveis e acionáveis por máquina. Os autores declaram explicitamente que o sistema proposto não é um substituto para as infraestruturas de publicação ou verificação existentes. Em vez disso, serve como uma "camada conectiva" que sistematiza o conhecimento de alinhamento informal existente em um recurso estruturado e consultável.

A significância reside na capacidade de:

1. Prover acesso unificado a resultados publicados e seus correspondentes formais.
2. Permitir a análise em larga escala de quanto da literatura matemática foi formalizada.
3. Criar uma base para vincular publicações a objetos de prova formais, apoiando potencialmente futuros fluxos de trabalho de matemática gerada por IA e híbridos humano-IA.

Os autores reconhecem limitações, observando que o processamento de PDF introduz ambiguidade, a qualidade da recuperação afeta a precisão da pontuação e que LLMs podem produzir correspondências espúrias. Consequentemente, eles enquadram o sistema como um "framework de melhor esforço" para alinhamento relacional, em vez de um mapeamento perfeitamente fiel, com a expectativa de que hiperlinks e mapeamentos serão eventualmente curados manualmente ou via processos supervisionados, de forma semelhante às práticas bibliográficas atuais.