Uma apresentação impecável pode estar errada. Um sistema pode parecer inteligente, persuadir especialistas e ainda esconder uma falha impossível de localizar a tempo. O caso da formalização do Último Teorema de Fermat coloca uma pergunta mais útil para a liderança: em decisões críticas, o resultado da IA pode ser verificado sem depender da confiança no próprio modelo?
O que aconteceu — e o que não aconteceu
Em 4 de setembro de 2026, a Anthropic anunciou que um sistema multiagente formalizou em Lean uma prova já conhecida do Último Teorema de Fermat [1]. É essencial preservar essa distinção: a IA não descobriu uma nova prova do teorema. A demonstração matemática foi construída por Andrew Wiles e completada com Richard Taylor nos anos 1990; os agentes converteram uma exposição simplificada desse trabalho em uma cadeia formal que o kernel do Lean pudesse verificar.
Segundo a publicação e o repositório, o trabalho durou 11 dias, envolveu dezenas de agentes, gerou aproximadamente 6 bilhões de tokens de saída, ultrapassou 13 milhões de linhas de Lean e terminou com 29.511 declarações utilizadas na prova principal [1][2]. Esses números descrevem escala computacional e artefatos produzidos. Não equivalem a custo financeiro, produtividade humana ou generalização para qualquer problema empresarial.
A força está na cadeia de evidência
A alegação central não repousa apenas na narrativa do fornecedor. O repositório público fixa versões de Lean e Mathlib, documenta a compilação e disponibiliza o artefato [2]. O kernel do Lean verificou a cadeia formal. O Comparator confrontou a declaração final com o teorema correspondente no Mathlib, inclusive quanto aos axiomas empregados [5]. E o Nanoda, um verificador independente escrito em Rust, conferiu 1.052.234 declarações sem relatar erros; essa etapa exigiu quatro pequenos patches descritos pelos autores como não enfraquecedores do sistema de tipos [1][2].
Kevin Buzzard, professor do Imperial College London e líder de um projeto concorrente de formalização do mesmo teorema, compilou o código e executou o Comparator. Sua avaliação independente foi que a verificação funciona, embora a realização acrescente pouco à matemática já conhecida e muito à capacidade de autoformalização [3]. Há contexto relevante: a Anthropic forneceu ao projeto acadêmico acesso a uma máquina de 500 GB, vínculo que precisa acompanhar a leitura do contraponto.
Da matemática ao negócio: saídas que carregam recibos
Poucas empresas precisam provar teoremas. Muitas precisam aprovar crédito, alterar uma política, liberar código, calcular um preço, reconciliar dados ou justificar uma decisão regulada. Nesses casos, a arquitetura mais confiável não pede que o mesmo modelo produza e valide uma resposta aberta. Ela transforma critérios em contratos e produz um artefato que um verificador determinístico, outra ferramenta ou uma pessoa habilitada possa reconstruir.
- Defina o que conta como aceitação antes de pedir a resposta à IA.
- Separe quem gera, quem verifica e quem possui autoridade para aceitar ou executar.
- Prenda versões, fontes, parâmetros e dependências ao artefato entregue.
- Registre falhas e incertezas como estado explícito, em vez de escondê-las numa resposta fluente.
- Use verificadores menores e independentes sempre que a natureza do problema permitir.
A IA não venceu sozinha: houve engenharia de sistema
O Prove2Me organizou tarefas como um grafo de dependências, distribuiu trabalho em paralelo, procurou lemas existentes e separou a formulação das declarações da construção das provas [1][4]. Tentativas anteriores falharam. O avanço ocorreu quando o problema ganhou estrutura, estado compartilhado, divisão de responsabilidades e um verificador capaz de recusar resultados inválidos. A lição é menos romântica — e mais útil — do que imaginar um modelo resolvendo tudo sozinho.
Verificação também tem custo
O repositório informa que uma compilação completa gerou cerca de 67 GB em artefatos, usou aproximadamente 220 GB em arquivos temporários, levou 5 horas e 32 minutos com 96 trabalhos paralelos e atingiu pico de 153 GB de memória. A execução do Comparator levou cerca de 15 horas e chegou a 230 GB [2]. A Anthropic não publicou o custo financeiro total. Portanto, este é um marco de capacidade, não uma receita econômica pronta para qualquer organização.
O que uma liderança pode fazer nos próximos 30 dias
- Escolha uma decisão de alto valor cujo resultado hoje dependa de revisão manual difusa.
- Escreva critérios de aceitação objetivos e identifique o que ainda exige julgamento humano.
- Projete um artefato verificável: testes, reconciliação, trilha de fontes, invariantes ou aprovação assinada.
- Meça não apenas a taxa de acerto, mas o tempo, o custo e a discordância da verificação.
- Autorize execução somente depois de provar que falhas ficam visíveis, contidas e reversíveis.
Limites e conflitos de interesse
A fonte principal é a própria Anthropic, desenvolvedora do sistema e interessada na repercussão do resultado [1]. O repositório aberto e as verificações externas reduzem, mas não eliminam, esse conflito. O experimento trata de um domínio formal em que respostas podem ser decididas por kernels; não demonstra o mesmo nível de verificabilidade para estratégia, comportamento humano, criatividade, medicina ou decisões jurídicas. A quantidade de tokens e linhas também não mede qualidade por si só.
Nota editorial e de responsabilidade
Este artigo combina fatos atribuídos às fontes com análise e recomendações profissionais do autor. Pontos de vista pessoais não são fatos comprovados; dados, denominadores, limites e conflitos relevantes são indicados quando disponíveis. O conteúdo é informativo e não substitui avaliação técnica, jurídica, financeira ou de risco. Tech Human e Trustyu atuam comercialmente em temas relacionados. Pesquisa, estrutura e redação tiveram assistência de IA; revisão factual, autoral e aprovação de publicação foram confirmadas por Fernando Parreiras em 05/09/2026.