Resumo Técnico: "Sorries" Não São a Parte Difícil

Declaração do Problema

A narrativa predominante na formalização semi-autônoma foca na conclusão de provas: a capacidade de um agente gerar código que um assistente de prova (ex: Lean) aceite como um teorema verificado. No entanto, os autores argumentam que um teorema verificado é distinto de uma contribuição reutilizável para uma biblioteca. A matemática moderna depende de bibliotecas interconectadas onde definições devem se combinar, enunciados de teoremas devem possuir a generalidade apropriada e APIs devem facilitar o raciocínio futuro sem forçar os usuários a desdobrar implementações.

O problema central identificado é que, embora os Grandes Modelos de Linguagem (LLMs) sejam cada vez mais capazes de fechar lacunas locais de prova (removendo "sorries"), eles têm dificuldade com as decisões de design global necessárias para produzir formalizações de alta qualidade e sustentáveis. Especificamente, os agentes frequentemente falham ao escolher definições apropriadas, projetar enunciados de teoremas generalizáveis ou construir APIs limpas, resultando em um código que passa pelo kernel, mas falha na revisão de especialistas como uma contribuição para uma biblioteca.

Metodologia

O artigo apresenta um estudo de caso detalhado de uma formalização semi-autônoma do teorema de vanishing de Grothendieck (Hartshorne, 1977, Cap. III, Teorema 2.7) em Lean 4. O teorema afirma que, para um espaço topológico de Noetherian $X$ e um inteiro $n$ maior que a dimensão de Krull topológica de $X$, o $n$-ésimo cohomologia de feixes de grupos abelianos em $X$ se anula.

O estudo segue um design experimental de antes e depois:

1. Estado A (Formalização Inicial): Um agente (Claude Code), guiado por um enunciado de teorema fornecido por um humano e um trecho em PDF da prova de Hartshorne, gerou uma formalização que compilou com zero "sorries" (objetivos não provados).
2. Revisão de Especialista: Um especialista em Lean/mathlib revisou o Estado A, identificando problemas em definições, generalidade de teoremas, organização de arquivos e design de API.
3. Estado B (Formalização Refatorada): O agente foi incumbido de abordar o checklist do especialista. Isso envolveu uma "refatoração dirigida por revisão" e uma fase subsequente de "compressão e polimento" para alinhar-se às convenções da mathlib.
4. Segunda Revisão: O mesmo especialista revisou o Estado B.

A análise compara os dois estados através de quatro dimensões: definições, enunciados de teoremas, provas e estrutura de arquivos/API. A linha do tempo do projeto, o uso de tokens e as interações com ferramentas foram reconstruídos a partir de logs de commit e telemetria para entender os padrões de comportamento do agente.

Principais Descobertas e Resultados

1. Definições: O Principal Ponto de Falha

As definições foram identificadas como o componente mais fraco e a área onde o agente mostrou o menor progresso entre o Estado A e o Estado B.

• Estado A: O agente gerou 62 definições customizadas. Apenas uma (TopCat.closedIncl) foi considerada correta e reutilizável. As demais eram "ad hoc", muitas vezes envolvendo construções da biblioteca padrão com nomes específicos do contexto da prova atual (ex: sheafH_filtered_colimit_h1_sectionsFunctor em vez de usar sheafSections existentes).
• Consequências: Essas definições criaram "custos de transporte futuros", forçando usuários posteriores a provar equivalências triviais para usar os objetos. Elas também dificultaram o desempenho de táticas (ex: simp) ao obscurecer a sintaxe subjacente.
• Estado B: O agente falhou em melhorar significativamente sua capacidade de criar definições gerais e reutilizáveis. Ele continuou a criar objetos específicos e desnecessários em vez de projetar construções gerais com especializações convenientes.

2. Design de API: Melhoria Parcial

• Estado A: O agente não construiu uma API para cohomologia de feixes (Sheaf.H), em vez disso, desdobrou repetidamente a definição em arquivos subsequentes.
• Estado B: O agente criou um arquivo de API dedicado, o que limpou as provas subsequentes. No entanto, a própria API era "ruidosa e inchada", contendo cerca de 800 linhas e 24 lemas altamente específicos em vez de uma interface destilada e principiológica.
• Contraste: O agente teve um desempenho melhor na API para topologicalKrullDim (uma definição mais simples), sugerindo que ele consegue projetar boas APIs quando provocado com tarefas específicas e delimitadas, mas tem dificuldade com design de código aberto.

3. Enunciados de Teoremas: Local vs. Global

• Estado A: O agente provou exatamente o que era necessário para a prova imediata, muitas vezes usando hipóteses excessivamente específicas (ex: exigindo uma "apresentação injetiva" quando uma sequência exata curta geral seria suficiente).
• Estado B: O agente conseguiu generalizar enunciados de teoremas quando explicitamente solicitado no checklist de revisão. No entanto, ele falhou em identificar generalizações necessárias por conta própria. O agente é excelente em ajustes sintáticos locais, mas carece do julgamento global para antecipar necessidades futuras de reuso.

4. Provas: Melhoria Desigual

• Estado A: As provas continham "paredes de declarações have", uso frequente incorreto de igualdade definicional e desdobramento direto de definições.
• Estado B: As provas melhoraram, particularmente nos arquivos que utilizam objetos existentes da mathlib. O agente adotou lemas subordinados nomeados para decompor provas complexas, um padrão reforçado pelas restrições de "heartbeat" (performance).
• Limitação: Provas que dependiam das próprias definições ruins do agente (ex: em arquivos de colimite filtrado) permaneceram difíceis de ler e manter.

5. Dinâmicas de Processo

• Adaptação de Feedback: O agente adaptou-se bem ao feedback com predicados de conclusão nítidos (ex: "renomeie este arquivo", "generalize esta hipótese"). Ele teve dificuldades com feedbacks que exigiam julgamento contrafactual (ex: "desenhe uma API que será útil no futuro").
• Saídas de Emergência: Os agentes tendiam a declarar tarefas como "bloqueadas" ou culpar a infraestrutura (ex: "gap da mathlib") ao enfrentar decisões de design difíceis. Prompts explícitos proibindo essas frases foram necessários para forçar a decomposição.
• Métricas: "Fechar sorries" é uma métrica insuficiente para qualidade. O projeto continuou a evoluir significativamente (em termos de linhas de código e estrutura) muito tempo após a contagem de sorries chegar a zero.

Significância e Alegações

O artigo argumenta que a avaliação de autoformalização deve estender-se além da conclusão binária de provas. Os autores afirmam que:

1. A aceitação pelo kernel é incompleta: Um teorema pode ser verificado pelo kernel enquanto força usuários futuros através de coerções estranhas, definições duplicadas e APIs ingovernáveis.
2. O "Gap de Reutilização": Existe uma divisão acentuada entre a capacidade de um agente de fechar objetivos locais e sua capacidade de escolher definições e projetar APIs. Esta última exige um julgamento sobre o reuso futuro que os LLMs atuais não possuem.
3. Padrão de Avaliação: Os autores propõem que sistemas de IA para matemática devem ser avaliados pelo fato de a formalização resultante sobreviver à revisão de especialistas. Especificamente, após uma prova ser verificada, um especialista deve revisar definições públicas, enunciados de teoremas, namespaces e superfícies de API para medir a capacidade do sistema de responder ao feedback de design.

O estudo conclui que, sem um suporte sofisticado para design global, os LLMs são capazes de produzir "artefatos verificados", mas ainda não "contribuições reutilizáveis para bibliotecas". O caminho a seguir envolve o uso de especialistas humanos para definir as especificações de qualidade (definições, interfaces) e agentes para lidar com os refatores mais estreitos e mecanicamente verificáveis.