Resumo Técnico: LeanMarathon

Definição do Problema

O artigo aborda o gargalo crítico na autoformalização de longo horizonte de matemática de nível de pesquisa. Embora os Grandes Modelos de Linguagem (LLMs) tenham avançado na geração de provas em linguagem natural e na verificação de lemas isolados, eles falham quando incumbidos de formalizar artigos de pesquisa inteiros. A dificuldade central não é meramente provar um único lema difícil, mas manter a durabilidade do agente ao longo de um processo de múltiplamente horas ou dias envolvendo centenas de declarações mutuamente dependentes.

As abordagens monolíticas atuais sofrem de três modos principais de falha:

1. Perda de Coerência: A tarefa é globalmente acoplada (como um Sudoku); um único agente tentando projetar, provar e reparar todo o grafo torna-se míope, frequentemente "roubando" de uma parte da prova para remendar outra.
2. Viés de Autoavaliação: Agentes solicitados a avaliar sua própria saída exibem excesso de confiança, falhando em detectar sutis derivações de formalização.
3. Irreversibilidade: Uma vez que o raciocínio de um agente se desvia do teorema alvo, o dano se acumula e o sistema não consegue se recuperar, levando à "podridão de contexto" (context rot), onde reparos locais corrompem o trabalho distante.

Sistemas existentes lutam contra o desvio de objetivo (goal drift - desviar do caminho lógico) e o fenômeno de estar perdido no meio (lost-in-the-middle - preso em subproblemas improdutivos), particularmente porque a formalização de nível de pesquisa carece de um blueprint pré-existente e detalhado, ao contrário da formalização de livros didáticos.

Metodologia: LeanMarathon

Os autores propõem o LeanMarathon, um suporte multi-agente projetado para tornar a autoformalização de longo horizonte legível, recuperável e resistente ao desvio. O sistema é construído sobre quatro princípios fundamentais:

1. Decomposição com DAG de Prova Dinâmica: O sistema não congela a decomposição inicial. Em vez disso, ele evolui um Grafo Acíclico Dirigido (DAG) de provas, dividindo nós grandes ou reparando aqueles mal formalizados até que as peças sejam pequenas o suficiente para agentes individuais.
2. Verificação Externa ou Determinística: Nenhum agente julga sua própria saída. O progresso é determinado exclusivamente por um verificador de CI determinístico e agentes externos.
3. Escopo de Ferramenta Restrito: Cada agente edita apenas uma região delimitada do código, garantindo que um erro resulte em um patch rejeitado em vez de corrupção global.
4. Informalizar enquanto Formaliza: Cada nó mantém tanto um tipo Lean quanto uma correspondente declaração em LaTeX, preservando a prosa. Um verificador impõe a paridade entre o grafo de dependência em linguagem natural e o grafo do elaborador formal para evitar divergência silenciosa.

O Blueprint

O artefato central é o Blueprint, um único arquivo Lean que serve como um esqueleto de prova formal, um grafo de prova em linguagem natural e um sistema de registro compartilhado. Ele contém enunciados de teoremas, lemas intermediários, definições e explicações em prosa. O grafo de dependência é inferido a partir dos metadados do elaborador do Lean e imposto contra as citações de LaTeX (\cref).

Agentes de Escopo de Contrato

O suporte emprega quatro agentes especializados, cada um com uma interface estreita e escopo de edição delimitado:

• Blueprinter: Lê a prova de origem e os enunciados alvo canônicos para construir o esqueleto Lean inicial. Ele escreve corpos de prova como placeholders sorry ou sorry_using. Seu objetivo é minimizar o "raio de reparo" (o número de declarações subsequentes afetadas se um enunciado estiver incorreto).
• Target-Reviewer: Audita o blueprint antes do início das provas. Ele compara o alvo canônico, o enunciado em LaTeX e o tipo Lean para garantir a fidelidade. Ele não pode editar o blueprint; discrepâncias são registradas como problemas (issues).
• Worker: Atribuído a um único nó de prova (cujos dependentes já foram provados). Ele opera em quatro fases:
  1. Auditoria de Malformalização: Verifica se o enunciado Lean corresponde à prosa e ao papel pretendido.
  2. Falsificação Barata: Tenta testes numéricos ou de limites para refutar a afirmação.
  3. Polimento de Enunciado: Edita apenas os campos de prosa para corresponder exatamente ao tipo Lean.
  4. Formalização: Tenta substituir o placeholder por uma prova completa dentro de uma região local congelada.
• Refiner: Repara defeitos no nível do blueprint reportados pelo Reviewer ou pelos Workers. Ele pode editar todo o blueprint, mas classifica os defeitos como desvio de blueprint (divergência da fonte) ou lacunas da fonte (prova incompleta na fonte). Ele segue uma árvore de decisão estrita, frequentemente substituindo corpos de prova completos por placeholders se eles não compilarem mais após um reparo.

Orquestração

O sistema opera em duas etapas:

1. Estágio 1 (Cold Start/Revisão de Alvo): Um loop aninhado onde o Blueprinter cria um esqueleto, o Target-Reviewer audita e o Refiner repara problemas até que os enunciados alvo sejam certificados como fiéis.
2. Estágio 2 (Descarga de Prova Orquestrada por DAG): O sistema identifica "folhas dinâmicas" (nós não provados com dependências satisfeitas) e os atribui a Workers em paralelo. Todos os Pull Requests (PRs) passam por um Gate de CI determinístico antes de serem mesclados. O Refiner processa problemas acumulados em rodadas. Este processo se repete até que o DAG esteja totalmente provado.

Principais Contribuições

1. Framework de Durabilidade de Agente: O artigo identifica a durabilidade do agente como o gargalo central e propõe um sistema de agentes falíveis com contenção de falhas. Ao separar a revisão de alvo adversária da descarga de prova paralela, transforma uma execução frágil de múltiplos dias em muitas transações curtas, paralelas e recuperáveis.
2. Formulação de DAG de Prova Dinâmica: Os autores introduzem uma formulação central onde um único blueprint atua como esqueleto formal, grafo de linguagem natural e sistema de registro. O suporte expande e repara este DAG dinamicamente, realizando a descarga a partir das folhas para cima, em paralelo.
3. Validação Empírica em Problemas de Pesquisa: O sistema é avaliado em dois artigos recentes cobrindo quatro problemas de Erdős (#1051, #1196, #164, #1217).

Resultados

O LeanMarathon foi avaliado em dois artigos de 2026 (Barreto et al., 2026; Alexeev et al., 2026) através de três execções autônomas:

• Taxa de Sucesso: Formalizou todos os sete teoremas alvo sem nenhum placeholder sorry.
• Escala: O sistema provou 258 lemas e teoremas no total.
• Desenvolvimento Incremental: O sistema conseguiu estender uma formalização concluída do problema #1196 para incluir os problemas #164 e #1217, reutilizando 59 nós sem alterações e adicionando 145 novos nós.
• Comparação: Uma linha de base de agente único comercial (Aristotle) falhou em ambos os artigos após dezenas de horas, deixando lacunas críticas (ex: o "conteúdo matemático mais profundo" dos artigos) não provados.
• Eficiência: Os PRs paralelos nunca entraram em conflito devido ao design de região editável congelada. O sistema localizou as falhas em nós individuais, impedindo que formalizações incorretas precoces consumissem computação subsequente.

Significância e Alegações

O artigo alega que a co-matemática confiável por IA requer não apenas provadores mais fortes, mas suportes duráveis que preservem a fidelidade do alvo ao longo de desenvolvimentos matemáticos longos.

• Confiabilidade: Ao impor verificações estruturais (ex: proximidade de lemas, paridade de dependência de prova) e impedir que agentes editem spans congelados, o sistema garante que o artefato formal permaneça um sistema de registro coerente.
• Valor Matemático: O processo de formalização atua como um "sinal matemático de verdade fundamental", expondo lacunas em provas publicadas (ex: hipóteses de somabilidade ausentes, passos não justificados em argumentos analíticos) que leitores humanos poderiam ignorar.
• Escalabilidade: A arquitetura demonstra que a autoformalização de nível de pesquisa é viável se o sistema for projetado para lidar com desvios e reparos localmente, em vez de depender de um agente monolítico para manter a coerência global.

Os autores concluem que o LeanMarathon representa um passo em direção a co-matemáticos de IA cujo trabalho de longa duração permanece legível, recuperável e verificável, desde que a biblioteca Lean subjacente (Mathlib) seja suficiente para o domínio.