# Claude va demostrar Fermat en 11 dies. Veredicte: SHIP IT.

Published: 2026-09-07

Claude va passar 11 dies i uns 6 mil milions de tokens escrivint una prova Lean de 13 milions de línies de l'Últim Teorema de Fermat —la primera verificada per ordinador de principi a fi— mentre que el matemàtic que l'ha estat formalitzant des del 2024 diu que "no ens diu essencialment res" matemàticament i està emocionat de totes maneres. El mateix dia: el número 1 mundial de Go, Shin Jin-seo, venç KataGo 2–1 amb un handicap de dues pedres. Veredicte: SHIP IT.

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

## Què cobreix aquest vídeo

- Claude formalitza l'Últim Teorema de Fermat a Lean 4
- RCE del sandbox de Chromium (CVE-2026-85046), explotada a la natura, recompensa de 1.000 $
- Shin Jin-seo venç KataGo amb un handicap de dues pedres

## Transcripció traduïda

Traduït de la narració original en anglès. L'àudio i els subtítols disponibles estan controlats per YouTube.

0:00 Fermat va dir que la seva meravellosa prova no cabria al marge, i avui Anthropic va publicar el marge: tretze milions de línies de Lean, cinc vegades la mida de Mathlib, demostrant un teorema que tots els matemàtics ja creien. Eren les deu o les onze a Tbilisi quan Anthropic va publicar, així que naturalment estava despert. Ahir Google va llançar Chrome 152 amb dotze correccions de seguretat, una d'elles un error de V8 ja explotat a la natura, i va pagar al reporter mil dòlars, que és menys que el sedan al qual arribarem més tard.

0:26 També ahir, Mullvad va dir que tancarà el seu DNS xifrat públic el 2 de novembre i pagarà a Quad9 perquè ho faci en el seu lloc, i aquest matí el compilador de Rust React es va tornar natiu a Vite, mentre que Hacker News va descobrir IBM Bob, un agent de codificació d'IA. Llavors Claude va formalitzar l'Últim Teorema de Fermat, i a la mateixa portada un gran mestre coreà va vèncer el motor de Go més fort de la Terra, així que avui la humanitat en va fer una de dues. En aquest vídeo: què va demostrar realment Claude, què va costar,

0:52 per què el matemàtic que va dedicar la seva carrera a això diu que no canvia res i està emocionat de totes maneres, i com un humà va vèncer la màquina a Go. És divendres, 4 de setembre, i això és The Daily Diff. L'Últim Teorema de Fermat: cap enter positiu a, b, c satisfà a elevat a n més b elevat a n igual c elevat a n per a qualsevol n superior a 2. Fermat ho va escriure en un marge al voltant de 1637 i va morir sense mostrar la seva feina, convertint-lo en el primer desenvolupador a tancar un tiquet amb 'funciona a la meva màquina'. Un premi de 100.000 marcs d'or el 1908 va atraure 621 proves

1:25 equivocades en el seu primer any, i Andrew Wiles finalment ho va aconseguir el 1995, en 129 pàgines que van trigar mesos a verificar els àrbitres. Formalitzar significa reescriure aquesta prova perquè Lean, un assistent de proves, pugui comprovar cada pas mecànicament, i Kevin Buzzard a l'Imperial ha liderat un esforç humà per fer exactament això des del 2024; el plànol només té 86 pàgines. La investigadora d'Anthropic Tianyi Peng hi va dirigir dotzenes d'agents Claude en el seu lloc, en una plataforma anomenada Prove2Me que manté un DAG d'enunciats de teoremes perquè els agents sàpiguen què han de demostrar a continuació, perquè sense ella els primers

2:00 eixams van perdre el compte de qui estava provant què, que és el que passa quan la teva capa d'orquestració és una regex amb un pressupost de màrqueting. Onze dies després el node arrel deia DEMOSTRAT: tretze milions de línies de Lean, 29.500 teoremes intermedis, uns sis mil milions de tokens de sortida d'un model intern més o menys comparable a Claude Fable 5.1. La compilació falla a menys que la prova es basi exactament en els tres axiomes estàndard de Lean: no, ho sento, no hi ha cap decisió nativa, no hi ha trampes. Comprovar-ho tampoc és barat: una

2:29 compilació des de zero va trigar cinc hores i mitja en 96 nuclis i 153 gigabytes de RAM, i els noms dels teoremes són generats per màquina, de manera que el repositori es descriu com a escrit per ser verificat en lloc de ser llegit, que també és com descriuria el Java empresarial. Ara la contradicció. La publicació d'Anthropic diu que Lean demostra la correcció sense cap mena de dubte. Kevin Buzzard, l'home a qui van guanyar, va compilar el repositori en una màquina de 500 gigabytes que Anthropic li va prestar, va confirmar que funcionava, i després va escriure,

2:56 cito, matemàticament aquest treball no ens diu essencialment res. Ja estava segur al 99,9 per cent que el teorema era cert, i la prova no afegeix cap matemàtica nova; el que mostra és el que l'autoformalització pot fer ara, i aquesta part l'entusiasma genuïnament. Se li va donar un milió de lliures durant cinc anys; Anthropic va trigar onze dies, i el càlcul ràpid d'un comentarista situa sis mil milions de tokens de sortida al preu de llista uns 300.000 dòlars, així que la màquina era més barata, tret que comptis amb l'entrenament de la màquina, cosa que ningú fa.

3:24 Millor detall: el correu electrònic va arribar mentre ell estava en un festival de música a Gal·les amb una barra de 4G, d'un nom del qual mai havia sentit parlar, així que el va descartar com una broma i el va llegir una setmana després, que és la resposta correcta a qualsevol assumpte que contingui una formalització d'extrem a extrem. Mentrestant, els humans van recuperar un punt. Shin Jin-seo, el número u mundial de Go, va vèncer a KataGo, el motor de Go de codi obert més potent, dos jocs a un a Seül amb un handicap de dues pedres, aproximadament la bretxa entre un professional d'elit i un professional novell.

3:50 La decisòria va ser una victòria d'11,5 punts en 221 moviments, mantenint una probabilitat de victòria del 99 per cent des de mitja partida, i es va emportar a casa 250 milions de wons, uns 170.000 dòlars, més un Genesis G90, així que la recompensa per vèncer una IA sobrehumana és 170 vegades la recompensa de Google per a una fugida del sandbox de Chrome. La seva explicació: al principi va copiar moviments de la IA i va perdre; va guanyar construint el tauler al seu propi estil, que és el consell més útil sobre IA que he sentit tot l'any, i va venir d'un joc de taula. Dues línies més en el diff.

4:22 El compilador Rust React d'oxc ja és natiu a Vite darrere d'una bandera; una base de codi de 1.036 fitxers va passar de 14,3 segons a 0,81 en el pas de compilació, majoritàriament eliminant Babel de package.json, que també és la meva rutina de cura de la pell. I IBM va llançar Bob, un soci de codificació d'IA que et saluda amb 'Hola, soc Bob', genera subagents, modernitza el codi de mainframe, i llança un producte d'anàlisi anomenat Bobalytics, així que en algun lloc un banc està molt emocionat i ningú va llegir la llicència.

4:51 Això és molt marge per un divendres; si preferiu llegir això que sentir-me dir-ho, el diff arriba a la vostra safata d'entrada cada matí — gratuït a The Daily Diff dot dev, enllaç a continuació. Així, el veredicte d'avui: SHIP IT. El nucli diu que sí, Buzzard diu que sí, les matemàtiques no van canviar, però la manera com comprovem les matemàtiques sí que ho ha fet. Aquest és el diff d'avui. Soc en Niko d'Axrisi.

5:09 Merge responsibly.

## Fonts

- [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