Claude provou Fermat em 11 dias. Veredito: SHIP IT.

O que este vídeo aborda

• Claude formaliza o Último Teorema de Fermat em Lean 4
• RCE do sandbox do Chromium (CVE-2026-85046), explorado ativamente, recompensa de 1.000 $
• Shin Jin-seo vence KataGo com um handicap de duas pedras

Transcrição traduzida

Traduzido da narração original em inglês. Áudio e legendas disponíveis são controlados pelo YouTube.

0:00 Fermat disse que a sua prova maravilhosa não caberia na margem, e hoje a Anthropic publicou a margem: treze milhões de linhas de Lean, cinco vezes o tamanho de Mathlib, provando um teorema em que todo o matemático já acreditava. Eram dez para as onze em Tbilisi quando a Anthropic publicou, por isso, naturalmente, eu estava acordado. Ontem, a Google lançou o Chrome 152 com doze correções de segurança, um deles um bug do V8 já explorado ativamente, e pagou ao repórter mil dólares, o que é menos do que a berlina que veremos mais tarde.

0:26 Também ontem, a Mullvad disse que vai encerrar o seu DNS público encriptado a 2 de novembro e pagar à Quad9 para o fazer em vez disso, e esta manhã o Rust React Compiler tornou-se nativo em Vite, enquanto o Hacker News descobriu o IBM Bob, um agente de codificação de IA. Depois, Claude formalizou o Último Teorema de Fermat, e na mesma página inicial um grande mestre coreano venceu o motor de Go mais forte da Terra, então hoje a humanidade marcou um em dois. Neste vídeo: o que Claude realmente provou, o que custou,

0:52 porque é que o matemático que passou a sua carreira nisto diz que não muda nada e está entusiasmado de qualquer forma, e como um humano venceu a máquina no Go. É sexta-feira, 4 de setembro, e este é The Daily Diff. Último Teorema de Fermat: nenhuns números inteiros positivos a, b, c satisfazem a elevado a n mais b elevado a n igual a c elevado a n para qualquer n acima de 2. Fermat rabiscou-o numa margem por volta de 1637 e morreu sem mostrar o seu trabalho, tornando-o o primeiro desenvolvedor a fechar um "ticket" com "funciona na minha máquina". Um prémio de 100.000 marcos de ouro em 1908 atraiu 621 provas erradas

1:25 no seu primeiro ano, e Andrew Wiles finalmente conseguiu em 1995, em 129 páginas que levaram meses aos revisores para verificar. Formalizar significa reescrever essa prova para que Lean, um assistente de prova, possa verificar cada passo mecanicamente, e Kevin Buzzard no Imperial tem liderado um esforço humano para fazer exatamente isso desde 2024; o projeto sozinho tem 86 páginas. O investigador da Anthropic, Tianyi Peng, apontou dezenas de agentes Claude para ele em vez disso, numa plataforma chamada Prove2Me que mantém um DAG de afirmações de teoremas para que os agentes saibam o que provar a seguir, porque sem ela os primeiros

2:00 enxames perdiam o rasto de quem estava a provar o quê, o que acontece quando a sua camada de orquestração é regex com um orçamento de marketing. Onze dias depois, o nó raiz dizia PROVADO: treze milhões de linhas de Lean, 29.500 teoremas intermédios, cerca de seis mil milhões de tokens de saída de um modelo interno aproximadamente comparável ao Claude Fable 5.1. A compilação falha a menos que a prova se baseie exatamente nos três axiomas padrão de Lean: sem desculpas, sem decisão nativa, sem batota. Verificá-lo também não é barato: uma

2:29 compilação do zero levou cinco horas e meia em 96 núcleos e 153 gigabytes de RAM, e os nomes dos teoremas são gerados por máquina, então o repositório descreve-se como escrito para ser verificado em vez de lido, o que também é como eu descreveria o Java empresarial. Agora, a contradição. A publicação da Anthropic diz que Lean demonstra a correção para além de qualquer dúvida. Kevin Buzzard, o homem que foi superado, compilou o repositório numa máquina de 500 gigabytes que a Anthropic lhe emprestou, confirmou que verifica, e depois escreveu,

2:56 citação, matematicamente este trabalho não nos diz essencialmente nada. Ele já tinha 99,9 por cento de certeza de que o teorema era verdadeiro, e a prova não adiciona matemática nova; o que ela mostra é o que a autoformalização pode fazer agora, e essa parte ele está genuinamente entusiasmado. Foi-lhe dado um milhão de libras ao longo de cinco anos; a Anthropic levou onze dias, e o cálculo rápido de um comentador coloca seis mil milhões de tokens de saída ao preço de tabela cerca de 300.000 dólares, então a máquina era mais barata, a menos que se conte a formação da máquina, o que ninguém faz.

3:24 Melhor pormenor: o e-mail chegou enquanto ele estava num festival de música no País de Gales com um único ponto de 4G, de um nome que ele nunca tinha ouvido falar, então ele ignorou-o como uma brincadeira e leu-o uma semana depois, o que é a resposta correta para qualquer linha de assunto que contenha formalização de ponta a ponta. Entretanto, os humanos recuperaram. Shin Jin-seo, o número um mundial de Go, venceu KataGo, o motor de Go de código aberto mais forte, dois jogos a um em Seul com um handicap de duas pedras, aproximadamente a diferença entre um profissional de topo e um profissional novato.

3:50 A partida decisiva foi uma vitória por 11,5 pontos em 221 movimentos, mantendo uma probabilidade de vitória de 99 por cento a partir da metade do jogo, e ele levou para casa 250 milhões de won, cerca de 170.000 dólares, mais um Genesis G90, então a recompensa por derrotar uma IA super-humana é 170 vezes a recompensa do Google por uma fuga de sandbox do Chrome. A sua explicação: no início ele copiou os movimentos da IA e perdeu; ele venceu ao construir o tabuleiro ao seu próprio estilo, que é o conselho mais útil sobre IA que ouvi este ano, e veio de um jogo de tabuleiro. Mais duas linhas no diff.

4:22 O Rust React Compiler da oxc está agora nativo no Vite atrás de uma flag; uma base de código de 1.036 ficheiros passou de 14,3 segundos para 0,81 na etapa de compilação, principalmente ao eliminar o Babel do package.json, que também é a minha rotina de cuidados com a pele. E a IBM lançou o Bob, um parceiro de codificação de IA que o cumprimenta com 'Olá, sou o Bob', gera subagentes, moderniza código de mainframe, e lança um produto de análise chamado Bobalytics, então em algum lugar um banco está muito entusiasmado e ninguém leu a licença.

4:51 É muita margem para uma sexta-feira; se preferir ler isto a ouvir-me dizê-lo, o diff chega à sua caixa de entrada todas as manhãs — gratuitamente em daily diff dot dev, link abaixo. Então, o veredito de hoje: SHIP IT. O kernel diz sim, o Buzzard diz sim, a matemática não mudou, mas a forma como verificamos a matemática acabou de mudar. Essa é a diferença de hoje. Sou o Niko da Axrisi.

5:09 Faça a fusão de forma responsável.

Fontes

1. Anthropic — Formalizing Fermat's Last Theoremwww.anthropic.com
2. The proof (Lean 4, Apache-2.0)github.com
3. Kevin Buzzard — FLT: Anthropic has beaten me to itxenaproject.wordpress.com
4. HN threadnews.ycombinator.com
5. KED Global — Shin defeats KataGowww.kedglobal.com
6. HNnews.ycombinator.com
7. Chrome 152 release notes (CVE-2026-85046)chromereleases.googleblog.com
8. NVDnvd.nist.gov
9. Mullvad — shutting down public encrypted DNSmullvad.net
10. Rust React Compiler native in Viteblog.master.dev
11. IBM Bobbob.ibm.com