Prova formal e saídas verificáveis: quando o verificador encerra a discussão

Um agente entrega uma resposta. Outro agente a revisa. Os dois concordam. Ainda assim, a conclusão pode estar errada porque ambos compartilham modelos, contexto, pressupostos ou falhas semelhantes.

O anúncio da Anthropic sobre a formalização do Último Teorema de Fermat oferece um caso raro: o artefato gerado por IA pôde ser recusado ou aceito por verificadores formais que não precisavam confiar na eloquência do modelo.

Estado: Evidence Brief aprovado para publicação. Este texto analisa um artefato público e propõe um padrão de arquitetura. Não afirma que a Trustyu Forge reproduziu o experimento, nem que esse desenho está implementado ou operando em todos os seus produtos.

Escopo correto da alegação

Em 4 de setembro de 2026, a Anthropic informou que seu sistema multiagente Prove2Me formalizou em Lean uma prova existente do Último Teorema de Fermat. A publicação da Anthropic descreve 11 dias de trabalho, dezenas de agentes, aproximadamente 6 bilhões de tokens de saída, mais de 13 milhões de linhas de Lean produzidas ao longo do processo e 29.511 declarações usadas na prova final.

A formulação precisa importa: os agentes não descobriram o teorema nem uma prova matemática nova. Eles converteram uma exposição simplificada da prova de Wiles e Taylor-Wiles em uma cadeia formal verificável. O repositório público fixa Lean 4.33.1 e Mathlib v4.33.0, fornece instruções de compilação e expõe os artefatos sob licença Apache-2.0.

Esses números não informam custo financeiro total, produtividade humana equivalente ou desempenho em outros domínios. São medidas do processo e do artefato neste caso.

Quatro camadas de verificação

1. O corpo formal

O Lean transforma cada passo em termos que precisam satisfazer o sistema de tipos. A resposta final não é aceita porque parece correta: precisa ser reconstruída pelo kernel.

2. O kernel do Lean

O repositório informa uma compilação de 60.475 módulos. O kernel verificou a cadeia usando três axiomas padrão. A superfície de confiança é menor do que a pilha inteira que produziu o código, mas não é zero: inclui o kernel, as versões fixadas, a cadeia de build e o ambiente.

3. O Comparator

O Comparator compara teoremas Lean até igualdade definicional. No caso, ele foi usado para conferir se a declaração final corresponde ao teorema esperado no Mathlib e se a lista de axiomas coincide. Isso evita um falso positivo comum em geração formal: provar um enunciado parecido, porém mais fraco ou diferente.

4. Um kernel independente

Segundo a Anthropic e o repositório, o Nanoda — verificador em Rust independente do kernel do Lean — conferiu 1.052.234 declarações sem erros. Foram necessários quatro pequenos patches, descritos como não enfraquecedores do sistema de tipos. Essa ressalva precisa permanecer junto da alegação; “verificador independente” não significa reprodução sem adaptação.

Kevin Buzzard, professor do Imperial College London e líder de um projeto relacionado de formalização, relata no Xena Project ter compilado o código e executado o Comparator com sucesso. É uma corroboração externa relevante. Também há contexto de relação: a Anthropic forneceu ao projeto acadêmico acesso a uma máquina de 500 GB.

Proof-carrying output para agentes

Em segurança de software, proof-carrying code descreve código acompanhado por evidência verificável de propriedades. O padrão pode ser generalizado com cuidado para agentes: uma saída que carrega prova inclui o resultado, as condições em que foi produzido e um artefato que um verificador independente consegue reconstruir.

Uma resposta de texto não se transforma em prova apenas por incluir uma justificativa. Para ser proof-carrying, a evidência precisa ter semântica definida, aceitar rejeição e reduzir a quantidade de confiança depositada no gerador.

spec versionada
      ↓
gerador probabilístico ──→ artefato candidato
                               ↓
                    verificador independente
                         ↙           ↘
                    rejeita        aceita
                       ↓              ↓
              evidência de falha   receipt assinado
                       └──────→ decisão humana/runtime

Um contrato mínimo de saída verificável

O contrato deve sobreviver a sessões, modelos e equipes. Ambientes isolados, estado explícito e evidências duráveis são propriedades do harness ao redor do agente, não qualidades mágicas do modelo. Elas ajudam a tornar falhas observáveis, mas não provam automaticamente que um produto está seguro ou pronto para operar. [HARNESS31-C2]

O que o Prove2Me ensina sobre orquestração

O paper do Prove2Me descreve um sistema neurossimbólico que organiza metas como um grafo dirigido acíclico, paraleliza subtarefas, busca e reutiliza lemmas e separa a proposição de declarações da construção de provas.

Esse desenho contém quatro lições transferíveis:

1. A dependência é uma entidade do sistema. Subtarefas só avançam quando seus pré-requisitos são satisfeitos.
2. O estado é compartilhado e versionado. Agentes não trabalham apenas sobre resumos conversacionais.
3. O verificador cria feedback objetivo. Falhas retornam ao ciclo sem precisar de uma avaliação subjetiva do próprio gerador.
4. Tentativas fracassadas são evidência. A Anthropic relata abordagens anteriores que não escalaram; o resultado dependeu de scaffold e decomposição, não apenas de mais capacidade de modelo.

Onde esse padrão cabe — e onde não cabe

Proof-carrying output é especialmente útil quando o domínio oferece invariantes verificáveis:

• compilação, tipos, testes e propriedades de software;
• reconciliação contábil e conservação de totais;
• aplicação de políticas e limites de acesso;
• transformações de dados com contratos de esquema;
• cálculos reproduzíveis e trilhas regulatórias;
• configurações que podem ser avaliadas por policy-as-code.

O padrão é mais limitado quando o resultado depende de gosto, negociação, contexto social, prognóstico humano ou categorias jurídicas abertas. Nesses casos, evidência estruturada continua útil, mas não elimina julgamento, disputa de interpretação ou responsabilidade profissional.

Custo de reprodução e limite operacional

O repositório informa que o build completo gerou cerca de 67 GB na pasta .lake, utilizou aproximadamente 220 GB para arquivos C temporários, levou 5 horas e 32 minutos com 96 trabalhos paralelos e atingiu pico de 153 GB de memória. O Comparator levou aproximadamente 15 horas e chegou a 230 GB.

Isso demonstra que verificabilidade também consome engenharia e infraestrutura. A Anthropic não publicou custo total do experimento. Seis bilhões de tokens não devem ser convertidos em preço sem conhecer modelos, descontos, cache, tentativas internas e infraestrutura. Para produto, o objetivo não é maximizar prova; é escolher a evidência proporcional à consequência e ao risco.

Gate técnico antes do release

Uma equipe pode usar este gate para um fluxo crítico:

1. O requisito está versionado e tem condições explícitas de rejeição?
2. O resultado material — não apenas o texto — é verificável?
3. O verificador é independente do gerador na dimensão de falha relevante?
4. Entrada, saída, versões e evidências estão ligados por digests?
5. Falha, inconclusão e timeout são estados distintos de sucesso?
6. A autoridade de release está separada da produção e da verificação?
7. O custo e a latência da verificação foram medidos no p95?
8. Existe fallback e o erro permanece contido e reversível?

Um gate aprovado não é evidência de produção observada. É autorização delimitada para a versão e o escopo avaliados.

Limitações, contrapontos e conflitos

• A Anthropic é a fonte principal e desenvolvedora do sistema; tem interesse comercial no resultado.
• O repositório aberto, os kernels e a avaliação de Buzzard fortalecem a alegação técnica, mas não constituem auditoria financeira ou reprodução por múltiplos grupos independentes.
• Buzzard considera que o trabalho acrescenta pouco à matemática conhecida e muito à autoformalização; sua análise também ocorre em um ecossistema que recebeu infraestrutura da Anthropic.
• O domínio matemático permite verificação formal. A mesma garantia não se transfere a decisões abertas.
• Linhas, tokens e quantidade de declarações medem volume, não valor isoladamente.
• O custo total, a energia consumida e a distribuição das tentativas fracassadas não foram divulgados.

Fontes e contexto editorial

1. Anthropic — Formalizing Fermat's Last Theorem in Lean. Fonte primária do fornecedor, publicada em 04/09/2026.
2. Anthropic — repositório fermats-last-theorem. Código, versões, instruções, métricas de build e licença.
3. Xena Project — FLT: Anthropic has beaten me to it. Corroboração e contraponto de Kevin Buzzard.
4. Prove2Me. Descrição do sistema neurossimbólico e da orquestração.
5. Lean Comparator. Implementação do comparador usado na checagem.

Nota editorial e de responsabilidade

Este texto combina fatos atribuídos às fontes com análise e proposta técnica do autor. Pontos de vista pessoais e profissionais não são fatos comprovados; dados, denominadores, limites e conflitos são indicados quando disponíveis. O conteúdo é informativo e não substitui avaliação técnica, matemática, jurídica, financeira ou de segurança. Tech Human e Trustyu atuam comercialmente em temas relacionados. Pesquisa, estrutura e redação tiveram assistência de IA; revisão factual, aprovação autoral e publicação foram confirmadas por Fernando Parreiras em 05/09/2026, sem revisão humana independente adicional.

Corte da pesquisa: 05/09/2026. Estado editorial: publicação especial extraordinária autorizada para 05/09/2026 às 19h21 BRT.