Resumo Técnico: MATHLIBLEMMA

1. Declaração do Problema

O ecossistema de matemática formal, particularmente o Lean e sua biblioteca Mathlib, enfrenta uma barreira de "última milha" que impede sua adoção como uma ferramenta cotidiana comparável ao LaTeX ou ao Maple. Embora os grandes modelos de linguagem (LLMs) tenham avançado na prova automática de teoremas, persiste um gargalo: a ausência de "lema de folclore". Estes são fatos intermediários que matemáticos em atividade usam rotineiramente e consideram óbvios (frequentemente aprendidos implicitamente a partir de livros didáticos ou prática), mas que não estão explicitamente presentes nas bibliotecas formais em um formato reutilizável.

Quando tais lemas estão ausentes, a formalização estagna em etapas triviais, mas necessárias, e os provadores baseados em LLM são forçados a reconstruir resultados do zero, em vez de invocá-los. Isso expande o espaço de busca, consome tokens de contexto e aumenta a probabilidade de alucinação e falha. As avaliações atuais frequentemente se concentram em conjuntos de problemas fixos de nível olímpico (por exemplo, MiniF2F), que estão atingindo saturação de desempenho, falhando em abordar a necessidade estrutural de expansão densa e reutilizável de bibliotecas.

2. Metodologia: O Pipeline MATHLIBLEMMA

Os autores introduzem o MATHLIBLEMMA, um pipeline modular baseado em LLM projetado para minerar, formalizar e provar proativamente esses lemas de folclore ausentes. O sistema opera através de quatro estágios distintos para fatorizar modos de falha (alucinação semântica, erros sintáticos e falha na busca de prova) em componentes ortogonais:

1. Módulo de Descoberta (Geração Consciente de Contexto):

   • Entrada: Arquivos de origem existentes do Mathlib (sementes).
   • Processo: Um LLM é instruído a brainstormar lemas ausentes plausíveis com base no contexto da semente, focando em lacunas estruturais e interações entre tópicos.
   • Saída: Declarações candidatas brutas em código Lean contendo espaços reservados sorry, sem tentar provas.

2. Módulo Julgador (Filtragem Semântica):

   • Processo: Um LLM atua como juiz para avaliar a correção matemática dos candidatos brutos, ignorando explicitamente a boa formação sintática do Lean.
   • Objetivo: Filtrar declarações matematicamente falsas ou sem sentido antes da verificação de kernel ou busca de prova dispendiosa.
   • Saída: Um veredito binário (correto/errado); apenas candidatos "corretos" prosseguem.

3. Módulo Formalizador (Reparo Guiado por Kernel):

   • Processo: O sistema interage com um servidor Lean (Kimina Lean server) para verificar o tipo das declarações filtradas semanticamente.
   • Loop: Se ocorrerem erros, um LLM repara iterativamente sintaxe, namespaces e argumentos implícitos com base nos diagnósticos do compilador. O loop termina quando a declaração compila sem diagnósticos de nível de erro ou quando um número máximo de tentativas é atingido.
   • Saída: Declarações Lean verificadas quanto ao tipo (ainda com sorry).

4. Módulo Provedor (Busca de Prova e Verificação):

   • Processo: Um LLM provedor tenta gerar uma prova completa para a declaração verificada quanto ao tipo.
   • Verificação: Tentativas bem-sucedidas devem passar em duas verificações:
     1. Verificação de Kernel Lean: O arquivo deve ser elaborado sem erros.
     2. Tela de Contorno de Prova: O código gerado é despojado de comentários e verificado para garantir que não contenha espaços reservados incompletos (sorry, admit, sorryAx) e nenhuma declaração de nível superior introduzida pelo modelo que adicione novas suposições (axiom, constant, opaque).
   • Loop: Provas falhas acionam um loop de gerar-verificar-reparar (até 2 rodadas de reparo).

3. Contribuições Principais

A. O Benchmark MATHLIBLEMMA

O pipeline gerou uma suíte de benchmark de 4.028 declarações Lean não triviais e verificadas quanto ao tipo, abrangendo três domínios:

• Fundacional: Análise real, estruturas discretas, probabilidade básica.
• Aplicado: Probabilidade avançada (martingalas), teoria da informação, análise convexa.
• Abstrato: Teoria das categorias, topologia algébrica, geometria diferencial.

Diferentemente de benchmarks anteriores, estes são conjecturas descobertas novelmente, sem provas de verdade-terreno pré-existentes. Os autores realizaram uma auditoria de provabilidade humana em uma amostra estratificada por semente de resíduos não resolvidos pelo modelo, encontrando que 78% eram matematicamente sólidos e prováveis por especialistas, indicando que muitas falhas são devidas às limitações atuais dos provadores e não a declarações falsas.

B. Uma Biblioteca de Folclore Verificada

O pipeline produziu um repositório de 1.506 provas verificadas pelo Lean que passaram na tela de contorno de prova. Isso serve como um ativo reutilizável para a comunidade.

• Validação de Upstreaming: Um pequeno esforço piloto submeteu seis lemas curados ao Mathlib. Três foram mesclados, fornecendo evidência externa de que saídas selecionadas podem atender aos padrões de bibliotecas de especialistas. Os exemplos mesclados incluem um lema de monotonicidade para o limite de Grönwall, um lema de compatibilidade de kernel na teoria da medida e um lema de congruência quase em toda parte para momentos centrais em probabilidade.

C. Avaliação de Modelos de Última Geração

O benchmark foi usado para avaliar vários modelos (GPT-5.1, variantes DeepSeek-R1, Goedel-Prover, Kimina-Prover, Qwen3) sob uma restrição de livro fechado (sem recuperação externa).

• Resultados: A união de todos os modelos provou 37,39% dos lemas, enquanto o melhor modelo individual (Goedel-Prover) provou 19,39%.
• Especialista vs. Generalista: O Goedel-Prover se destacou em domínios Fundacionais (27,42%), mas lutou em domínios Abstratos (8,24%), enquanto o GPT-Raciocínio mostrou desempenho mais consistente entre os domínios.
• Diversidade: A lacuna significativa entre o melhor modelo único e o desempenho da união sugere que sistemas futuros devem priorizar a combinação de arquiteturas diversas.

4. Significado e Alegações

O artigo alega que o MATHLIBLEMMA representa uma mudança no papel dos LLMs, de consumidores passivos de bibliotecas formais para contribuintes ativos em sua expansão.

• Abordando a Lacuna da Última Milha: Ao minerar proativamente o "tecido conectivo" da matemática, o trabalho aborda a barreira estrutural de lemas de folclore ausentes que limita a usabilidade dos assistentes de prova.
• Metodologia Construtiva: O framework fornece uma metodologia construtiva para expansão automatizada de bibliotecas, validada tanto pelo upstreaming bem-sucedido de provas no Mathlib quanto pela alta taxa de validade dos resíduos auditados por humanos.
• Mudança de Benchmarking: Desloca o foco da avaliação da resolução de quebra-cabeças isolados e difíceis (problemas olímpicos) para a tarefa fundamental de formalizar a vasta quantidade de fatos de fundo rotineiros que os matemáticos humanos dão como garantidos.

Os autores reconhecem limitações, incluindo a dependência da unicidade sintática para filtragem de novidade (potencialmente perdendo duplicatas semânticas), a falta de verificações de consistência semântica no loop de reparo e a necessidade de curadoria humana quanto à nomenclatura, posicionamento e generalidade antes da integração final no Mathlib. Eles posicionam o trabalho como um passo em direção à expansão assistida por IA de bibliotecas matemáticas formais, em vez de uma solução totalmente autônoma.