# Claude demostrou Fermat en 11 días. Veredicto: SHIP IT.

Published: 2026-09-07

Claude pasou 11 días e uns 6.000 millóns de tokens escribindo unha proba Lean do Último Teorema de Fermat de 13 millóns de liñas —a primeira verificada por ordenador de principio a fin— mentres o matemático que o está a formalizar desde 2024 di que «non nos di esencialmente nada» matematicamente e está emocionado de todos os xeitos. O mesmo día: o número 1 do mundo de Go, Shin Jin-seo, vence a KataGo 2-1 cun hándicap de dúas pedras. Veredicto: SHIP IT.

Canonical: https://thedailydiff.dev/gl/video/2026-09-04-fermat-lean/

## Que abrangue este vídeo

- Claude formaliza o Último Teorema de Fermat en Lean 4
- RCE na sandbox de Chromium (CVE-2026-85046), explotado na práctica, recompensa de 1.000 $
- Shin Jin-seo vence a KataGo cun hándicap de dúas pedras

## Transcrición traducida

Traducido da narración orixinal en inglés. O audio e os subtítulos dispoñibles son controlados por YouTube.

0:00 Fermat dixo que a súa marabillosa proba non cabería na marxe, e hoxe Anthropic publicou a marxe: trece millóns de liñas de Lean, cinco veces o tamaño de Mathlib, probando un teorema no que xa cría todo matemático. Eran as dez para as once en Tbilisi cando Anthropic publicou, así que, naturalmente, eu estaba esperto. Orixe: Google enviou onte Chrome 152 con doce correccións de seguridade, unha delas un erro de V8 xa explotado na práctica, e pagoulle ao reporteiro mil dólares, o que é menos que o sedán ao que chegaremos máis tarde.

0:26 Tamén onte, Mullvad dixo que pechará o seu DNS público cifrado o 2 de novembro e pagará a Quad9 para que o faga en vez diso, e esta mañá o Rust React Compiler volveuse nativo en Vite, mentres Hacker News descubría IBM Bob, un axente de codificación de IA. Entón Claude formalizou o Último Teorema de Fermat, e na mesma páxina principal un gran mestre coreano venceu o motor de Go máis forte da Terra, así que hoxe a humanidade foi un para dous. Neste vídeo: o que Claude demostrou realmente, o que custou,

0:52 por que o matemático que dedicou a súa carreira a isto di que non cambia nada e está emocionado de todos os xeitos, e como un humano venceu á máquina en Go. É venres, 4 de setembro, e isto é The Daily Diff. Último Teorema de Fermat: ningún número enteiro positivo a, b, c satisfai a elevado a n máis b elevado a n igual a c elevado a n para calquera n maior que 2. Fermat garabateouno nunha marxe arredor de 1637 e morreu sen amosar o seu traballo, facéndoo o primeiro desenvolvedor en pechar un ticket con funciona na miña máquina. Un premio de 100.000 marcos de ouro en 1908 atraeu 621 probas erróneas

1:25 no seu primeiro ano, e Andrew Wiles finalmente conseguiuno en 1995, en 129 páxinas que lles levaron aos árbitros meses en verificar. Formalizar significa reescribir esa proba para que Lean, un asistente de probas, poida comprobar cada paso mecanicamente, e Kevin Buzzard en Imperial liderou un esforzo humano para facer exactamente iso desde 2024; o proxecto só ten 86 páxinas. O investigador de Anthropic Tianyi Peng dirixiu decenas de axentes de Claude a iso en vez diso, nunha plataforma chamada Prove2Me que mantén un DAG de enunciados de teoremas para que os axentes saiban que probar a continuación, porque sen ela as primeiras

2:00 agrupacións perderon o rastro de quen estaba a probar que, que é o que acontece cando a túa capa de orquestración é regex cun orzamento de márketing. Once días despois, o nó raíz dicía PROBADO: trece millóns de liñas de Lean, 29.500 teoremas intermedios, uns seis mil millóns de tokens de saída dun modelo interno máis ou menos comparable a Claude Fable 5.1. A compilación falla a menos que a proba se base exactamente nos tres axiomas estándar de Lean: non, desculpe, sen decisión nativa, sen trampas. Comprobalo tampouco é barato: unha compilación

2:29 desde cero levou cinco horas e media en 96 núcleos e 153 gigabytes de RAM, e os nomes dos teoremas son xerados por máquina, polo que o repositorio descríbese como escrito para ser comprobado en lugar de lido, que é tamén como eu describiría o Java empresarial. Agora a contradición. A publicación de Anthropic di que Lean demostra a corrección sen dúbida. Kevin Buzzard, o home ao que lle gañaron, compilou o repositorio nunha máquina de 500 gigabytes que Anthropic lle prestou, confirmou que se verifica, e despois escribiu,

2:56 cita, matematicamente este traballo non nos di esencialmente nada. Xa estaba 99,9 por cento seguro de que o teorema era certo, e a proba non engade novas matemáticas; o que mostra é o que a autoformalización pode facer agora, e esa parte o emociona de verdade. Déronlle un millón de libras durante cinco anos; Anthropic tardou once días, e os cálculos de servilleta dun comentarista poñen seis mil millóns de tokens de saída a prezo de lista arredor de 300.000 dólares, polo que a máquina era máis barata, a non ser que contes o adestramento da máquina, o que ninguén fai.

3:24 Mellor detalle: o correo electrónico chegou mentres estaba nun festival de música en Gales con unha barra de 4G, dun nome do que nunca escoitara falar, así que o descartou como unha brincadeira e leuno unha semana despois, que é a resposta correcta a calquera asunto que conteña formalización de extremo a extremo. Mentres tanto, os humanos recuperaron un. Shin Jin-seo, o número un mundial en Go, venceu a KataGo, o motor de Go de código aberto máis forte, dúas partidas a unha en Seúl cun hándicap de dúas pedras, aproximadamente a diferenza entre un profesional de alto nivel e un profesional novato.

3:50 O desempate foi unha vitoria de 11,5 puntos en 221 movementos, mantendo unha probabilidade de vitoria do 99 por cento dende a metade da partida, e levou a casa 250 millóns de wons, uns 170.000 dólares, máis un Genesis G90, polo que a recompensa por vencer a unha IA superhumana é 170 veces a recompensa de Google por un escape da sandbox de Chrome. A súa explicación: ao principio copiou movementos da IA e perdeu; gañou construíndo o taboleiro ao seu propio estilo, que é o consello máis útil sobre IA que escoitei durante todo o ano, e veu dun xogo de mesa. Dúas liñas máis no diff.

4:22 O Rust React Compiler de oxc agora é nativo en Vite detrás dunha soa bandeira; unha base de código de 1.036 ficheiros pasou de 14,3 segundos a 0,81 no paso de compilación, principalmente eliminando Babel de package.json, que tamén é a miña rutina de coidado da pel. E IBM lanzou a Bob, un compañeiro de codificación de IA que te saúda con Ola, son Bob, xera subaxentes, moderniza o código do mainframe, e envía un produto de análise chamado Bobalytics, así que nalgún lugar un banco está moi emocionado e ninguén leu a licenza.

4:51 Iso é moita marxe para un venres; se prefires ler isto que escoitarme dicilo, o diff chega á túa caixa de entrada cada mañá — de balde en the daily diff dot dev, ligazón debaixo. Así, o veredicto de hoxe: SHIP IT. O kernel di que si, Buzzard di que si, as matemáticas non cambiaron, pero a forma en que revisamos as matemáticas si o fixo. Ese é o diff de hoxe. Son Niko de Axrisi.

5:09 Fusionar con responsabilidade.

## Fontes

- [Anthropic — Formalizing Fermat's Last Theorem](https://www.anthropic.com/research/formalizing-fermats-last-theorem) — www.anthropic.com
- [The proof (Lean 4, Apache-2.0)](https://github.com/anthropics/fermats-last-theorem) — github.com
- [Kevin Buzzard — FLT: Anthropic has beaten me to it](https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/) — xenaproject.wordpress.com
- [HN thread](https://news.ycombinator.com/item?id=49568506) — news.ycombinator.com
- [KED Global — Shin defeats KataGo](https://www.kedglobal.com/artificial-intelligence/newsView/ked202607210007) — www.kedglobal.com
- [HN](https://news.ycombinator.com/item?id=49544762) — news.ycombinator.com
- [Chrome 152 release notes (CVE-2026-85046)](https://chromereleases.googleblog.com/2026/09/stable-channel-update-for-desktop_01882797386.html) — chromereleases.googleblog.com
- [NVD](https://nvd.nist.gov/vuln/detail/cve-2026-85046) — nvd.nist.gov
- [Mullvad — shutting down public encrypted DNS](https://mullvad.net/en/blog/shutting-down-our-public-encrypted-dns-servers-and-sponsoring-quad9-instead) — mullvad.net
- [Rust React Compiler native in Vite](https://blog.master.dev/react-now-rusted-all-the-way-out/) — blog.master.dev
- [IBM Bob](https://bob.ibm.com/) — bob.ibm.com