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 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 do Mathlib, provando um teorema que todo matemático já acreditava. Eram dez para as onze em Tbilisi quando a Anthropic postou, então naturalmente eu estava acordado. Ontem o Google lançou o Chrome 152 com doze correções de segurança, uma delas um bug do V8 já explorado ativamente, e pagou ao repórter mil dólares, o que é menos que o sedã que veremos mais tarde.

0:26 Também ontem, a Mullvad disse que está desativando seu DNS público criptografado em 2 de novembro e pagando o Quad9 para fazê-lo, e esta manhã o Rust React Compiler foi nativo no Vite, enquanto o Hacker News descobriu o IBM Bob, um agente de codificação de IA. Então Claude formalizou o Último Teorema de Fermat, e na mesma primeira página um grande mestre coreano venceu o motor de Go mais forte da Terra, então hoje a humanidade fez um em dois. Neste vídeo: o que Claude realmente provou, quanto custou,

0:52 por que o matemático que dedicou sua carreira a isso diz que não muda nada e está emocionado mesmo assim, e como um humano venceu a máquina no Go. É sexta-feira, 4 de setembro, e este é o The Daily Diff. Último Teorema de Fermat: nenhum número inteiro positivo a, b, c satisfaz a elevado a n mais b elevado a n igual a c elevado a n para qualquer n acima de 2. Fermat rabiscou isso em uma margem por volta de 1637 e morreu sem mostrar 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

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

2:00 enxames perdiam o controle de quem estava provando o quê, que é o que acontece quando sua camada de orquestração é regex com um orçamento de marketing. Onze dias depois, o nó raiz lia PROVED: treze milhões de linhas de Lean, 29.500 teoremas intermediários, cerca de seis bilhõ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 do Lean: sem desculpas, sem 'decide' nativo, sem trapaça. 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 se descreve como escrito para ser verificado em vez de lido, que é também como eu descreveria o Java corporativo. Agora a contradição. A postagem da Anthropic diz que Lean demonstra a correção sem sombra de dúvida. Kevin Buzzard, o homem que foi vencido nisso, compilou o repositório em uma máquina de 500 gigabytes que a Anthropic lhe emprestou, confirmou que ele funciona, e então escreveu,

2:56 citando, 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 nenhuma matemática nova; o que ela mostra é o que a autoformalização pode fazer agora, e essa parte ele está genuinamente empolgado. Ele recebeu um milhão de libras ao longo de cinco anos; a Anthropic levou onze dias, e o cálculo de um comentarista coloca seis bilhões de tokens de saída a preço de tabela. cerca de 300.000 dólares, então a máquina era mais barata, a menos que você conte o treinamento da máquina, o que ninguém faz.

3:24 Melhor detalhe: o e-mail chegou enquanto ele estava em um festival de música em Gales com um único ponto de 4G, de um nome que ele nunca tinha ouvido falar, então ele descartou como uma brincadeira e leu uma semana depois, que é a resposta correta para qualquer linha de assunto contendo formalização ponta a ponta. Enquanto isso, os humanos conseguiram uma vitória. Shin Jin-seo, o número um do mundo no Go, venceu KataGo, o mais forte motor de Go de código aberto, dois jogos a um em Seul com um handicap de duas pedras, aproximadamente a diferença entre um profissional de ponta 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% a partir do meio do jogo, e ele levou para casa 250 milhões de wons, 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. Sua explicação: no início ele copiou movimentos da IA e perdeu; ele venceu ao construir o tabuleiro em seu próprio estilo, que é o conselho mais útil sobre IA que eu ouvi o ano todo, e veio de um jogo de tabuleiro. Mais duas linhas no diff.

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

4:51 Isso é muita margem para uma sexta-feira; se você preferir ler isso a me ouvir dizer, o diff chega na sua caixa de entrada todas as manhãs — grátis em the daily diff dot dev, link abaixo. Então, o veredito de hoje: SHIP IT. O kernel diz sim, Buzzard diz sim, a matemática não mudou, mas a forma como verificamos a matemática acabou de mudar. Esse é o diff de hoje. Eu sou Niko da Axrisi.

5:09 Faça merges com responsabilidade.

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