Treze milhões de linhas na margem: o que faz deste o bom caso

Sobre: “Formalizing Fermat’s Last Theorem” — Anthropic, 4 de setembro de 2026. O anúncio · O comentário de Kevin Buzzard

Onze dias, mais de treze milhões e quatrocentas mil linhas de Lean, vinte e nove mil e quinhentos teoremas intermediários e cerca de seis bilhões de tokens de saída. Com isso, várias dezenas de agentes de Claude produziram a primeira demonstração do último teorema de Fermat verificada integralmente por computador, e fecharam de passagem a lista de cem teoremas que Freek Wiedijk mantinha aberta há vinte anos. O matemático que dirige o projeto de formalizar esse mesmo teorema revisou o resultado e escreveu que, matematicamente, isso não nos diz essencialmente nada. Ele tem razão, e é exatamente por isso que vale a pena olhar.

O que há dentro do artefato

A versão que circula — a máquina resolveu em onze dias o que levou sete anos a Wiles — é falsa nas duas metades, e a própria Anthropic não a sustenta. Andrew Wiles demonstrou o teorema em 1995, em cento e vinte e nove páginas que levaram meses de revisão e às quais foi preciso remendar, um ano depois, um buraco encontrado durante esse processo. O que os agentes fizeram não foi encontrar uma demonstração, e sim transcrever uma: seguiram a exposição simplificada de Darmon, Diamond e Taylor e a despejaram numa linguagem cujo compilador não aceita nada por confiança. Os onze dias são tempo de relógio de dezenas de agentes em paralelo, coordenados pelo Prove2Me — uma plataforma aberta do grupo de Tianyi Peng em Columbia que mantém o grafo de dependências entre teoremas e diz a cada agente o que falta —, com uma intervenção humana limitada a instruções ocasionais de altíssimo nível, da ordem de o jacobiano como esquema parece prioritário.

O resultado, além disso, é mais estreito do que a manchete sugere: a formalização cobre os expoentes primos maiores ou iguais a dezessete, e o resto já estava feito por humanos.¹ Buzzard, que havia declarado antes de tudo isso estar 99,9% seguro de que a demonstração de Fermat estava correta, não mudou essa cifra ao ler o repositório. Não há conhecimento matemático novo aqui. Há um artefato de engenharia numa escala que não existia há um mês, e o que ele produz não é conhecimento sobre Fermat, e sim sobre o que esses sistemas conseguem fazer quando alguém coloca do outro lado algo capaz de lhes dizer não.

O núcleo não pergunta quem escreveu

A Anthropic escreve, numa frase que na sua prosa institucional é quase uma confissão, que a formalização é um lugar onde eles se sentem inequivocamente bem quanto ao papel da IA. Vale reconstruir por quê antes de discutir, porque a razão é boa e não tem nada a ver com as virtudes do modelo. O Lean verifica cada passo contra um núcleo minúsculo que admite apenas três axiomas, e esse núcleo é indiferente à procedência do que revisa: não sabe se as linhas foram escritas por um doutorando, por um enxame de agentes ou por um gerador aleatório com muita sorte, e seu veredito custa algumas horas de computação, ao passo que produzir o que ele revisa custou seis bilhões de tokens.² Um produtor não confiável acoplado a um verificador barato, independente e hostil resulta num sistema confiável. É toda a mágica, e é uma propriedade do domínio, não do modelo.

O que sobrevive da objeção habitual — que ninguém leu os treze milhões de linhas e portanto ninguém sabe o que elas dizem — é menor e mais preciso do que parece. O núcleo certifica que as linhas implicam o enunciado a partir dos axiomas; não certifica que o enunciado seja aquele que se queria demonstrar. Por isso a equipe rodou uma ferramenta comparadora contra a formulação que a Mathlib tem do teorema, e por isso Buzzard foi olhar o enunciado. Esse passo, o mais curto de todo o processo, é o único irredutivelmente humano, e não há quantidade de tokens que o encurte: alguém precisa responder se o que ficou escrito acima dos treze milhões de linhas diz o que o mundo entende por não existem inteiros positivos que satisfaçam a equação. Toda a confiabilidade do artefato se apoia numa leitura de três linhas.

Um presente que o comum não consegue levantar

Nada disso acontece sem a Mathlib. A biblioteca comunitária sobre a qual a demonstração se apoia foi escrita ao longo de anos por centenas de matemáticos, em boa medida sem que ninguém lhes pagasse por isso; o repositório da Anthropic credita cento e seis arquivos tomados do projeto FLT de Buzzard no Imperial College — financiado pelo EPSRC britânico com um milhão de libras em cinco anos — e do projeto flt-regular. A demonstração resultante é mais de cinco vezes o tamanho da Mathlib e demora quase vinte vezes mais para compilar, numa máquina de noventa e seis núcleos. Está no GitHub, com licença aberta, e provavelmente vai ficar por lá.

Essa é a parte que convém olhar devagar, porque não é um cercamento e dizê-lo assim seria mais cômodo do que exato. Não levaram nada: a Mathlib segue inteira, o código está publicado e, num ano em que os lançamentos de modelos consistiram em escolher qual camada se abre e qual se cobra, um repositório completo e auditável é mais do que costuma aparecer. O problema é de outra ordem. A Mathlib é um comum porque pode ser mantida: alguém lê um arquivo, entende o que ele faz, generaliza, refatora, discute o nome de um lema no Zulip. Treze milhões e quatrocentas mil linhas escritas para passar no compilador não admitem esse tratamento, e Buzzard supõe — com boas razões — que a Anthropic não fará o trabalho de convertê-las em algo que a comunidade possa absorver. Seus dois objetivos declarados, levar à Mathlib os objetos fundamentais da teoria dos números moderna e montar um documento dinâmico que permita a um humano percorrer a demonstração, seguem sendo dele e seguem pendentes. Um comum não se mede pelo que se pode baixar, e sim pelo que alguém pode sustentar; por esse critério, o que voltou ao comum não é a demonstração, e sim a notícia de que a demonstração é possível.

Três assinaturas

Há um segundo experimento no anúncio que importa mais a um leitor da região do que os treze milhões de linhas: um grupo de agentes rodando sobre três assinaturas pessoais do Claude Max, coordenados pela mesma plataforma, formalizou em três dias o teorema dos três primos de Vinogradov. Isso não é demonstração de força; é uma mudança no preço de entrada, e precisa ser concedida por inteiro. Até esta semana, a formalização era o único ramo da matemática contemporânea cuja barreira era o tempo e não o capital: o Lean roda num notebook, a Mathlib é gratuita, e a comunidade aceita contribuições de qualquer pessoa cujo código compile. Para departamentos que não vão comprar um cluster de GPUs nesta década, era a porta aberta — segue aberta, e agora se atravessa mais rápido.

A objeção não é sobre o acesso à ferramenta, e sim sobre a unidade de medida. Se o que era uma tese de doutorado em formalização passa a ser três dias de agentes, então o que conta como um projeto no campo é fixado por quem pode pagar o maior enxame, e a distância entre três assinaturas e várias dezenas de agentes sobre um modelo interno não é de preço, e sim de disponibilidade: o modelo que fez Fermat não está à venda.³ Convém também nomear o que aqui não existe, porque o vocabulário crítico se gasta quando usado por reflexo: não houve extração de dados do Sul, nem trabalho fantasma de anotação, nem um corpus local convertido em insumo. A assimetria é de outro tipo, mais simples e mais difícil de reverter, e consiste em que a capacidade que produziu o resultado não pode ser hospedada aqui nem comprada lá fora.

O que mais tem núcleo

A lição transferível destes onze dias não é que a máquina faz matemática. É um critério, e mais exigente do que parece: a IA funciona sem supervisão onde existe um verificador barato em relação à produção, independente de quem produz e público. Vale percorrer com esse critério na mão os desdobramentos que estão efetivamente em discussão na região. Um sistema de concessão de benefícios sociais não tem verificador barato: comprovar que um indeferimento foi correto custa mais do que produzi-lo, e o afetado descobre quando a transferência não chega. Um corretor automático de provas não tem verificador independente: quem o audita é quem o comprou. Uma triagem médica não tem verificador público: a verdade chega meses depois, dispersa em prontuários que ninguém cruza. Nos três casos o desdobramento acontece assim mesmo, e a diferença em relação a Fermat não é de risco nem de ambição, e sim de infraestrutura epistêmica.

Lean e Mathlib vêm sendo construídos há mais de uma década, em boa parte com trabalho voluntário e financiamento público, e sem esse núcleo o resultado desta semana não seria um resultado, e sim um arquivo de treze milhões de linhas em que ninguém teria motivo para acreditar. A pergunta que fica aberta não é se a máquina demonstra teoremas. É quanto tempo leva construir um núcleo, com que dinheiro e sob responsabilidade de quem, quando o que há para verificar não são teoremas, e sim processos administrativos.