Claude demostró Fermat en 11 días. Veredicto: SHIP IT.

Qué cubre este vídeo

• Claude formaliza el Último Teorema de Fermat en Lean 4
• RCE en sandbox de Chromium (CVE-2026-85046), explotado activamente, recompensa de 1.000 $
• Shin Jin-seo vence a KataGo con un hándicap de dos piedras

Transcripción traducida

Traducido de la narración original en inglés. El audio y los subtítulos disponibles están controlados por YouTube.

0:00 Fermat dijo que su maravillosa prueba no cabría en el margen, y hoy Anthropic publicó el margen: trece millones de líneas de Lean, cinco veces el tamaño de Mathlib, probando un teorema que todo matemático ya creía. Eran de diez a once en Tiflis cuando Anthropic publicó, así que naturalmente estaba despierto. Ayer Google lanzó Chrome 152 con doce correcciones de seguridad, uno de ellos un error de V8 ya explotado activamente, y pagó al reportero mil dólares, que es menos que el sedán del que hablaremos más tarde.

0:26 También ayer, Mullvad dijo que cerrará su DNS público cifrado el 2 de noviembre y que pagará a Quad9 para que lo haga en su lugar, y esta mañana el Rust React Compiler se volvió nativo en Vite, mientras que Hacker News descubrió IBM Bob, un agente de codificación de IA. Luego Claude formalizó el Último Teorema de Fermat, y en la misma portada un gran maestro coreano venció al motor de Go más fuerte de la Tierra, así que hoy la humanidad fue uno de dos. En este video: qué probó realmente Claude, cuánto costó,

0:52 por qué el matemático que dedicó su carrera a esto dice que no cambia nada y está encantado de todos modos, y cómo un humano venció a la máquina en Go. Es viernes, 4 de septiembre, y esto es The Daily Diff. Último Teorema de Fermat: no hay enteros positivos a, b, c que satisfagan a elevado a n más b elevado a n igual a c elevado a n para cualquier n superior a 2. Fermat lo garabateó en un margen alrededor de 1637 y murió sin mostrar su trabajo, convirtiéndolo en el primer desarrollador en cerrar un ticket con "funciona en mi máquina". Un premio de 100.000 marcos de oro en 1908 atrajo 621 pruebas

1:25 incorrectas en su primer año, y Andrew Wiles finalmente lo consiguió en 1995, en 129 páginas que los revisores tardaron meses en verificar. Formalizar significa reescribir esa prueba para que Lean, un asistente de pruebas, pueda verificar cada paso mecánicamente, y Kevin Buzzard en Imperial ha liderado un esfuerzo humano para hacer exactamente eso desde 2024; el plan por sí solo ocupa 86 páginas. El investigador de Anthropic, Tianyi Peng, dirigió docenas de agentes Claude a ello en su lugar, en una plataforma llamada Prove2Me que mantiene un DAG de declaraciones de teoremas para que los agentes sepan qué probar a continuación, porque sin ella los primeros

2:00 enjambres perdieron la pista de quién estaba probando qué, que es lo que sucede cuando tu capa de orquestación es una expresión regular con un presupuesto de marketing. Once días después, el nodo raíz decía PROBADO: trece millones de líneas de Lean, 29.500 teoremas intermedios, aproximadamente seis mil millones de tokens de salida de un modelo interno aproximadamente comparable a Claude Fable 5.1. La compilación falla a menos que la prueba se base exactamente en los tres axiomas estándar de Lean: no lo siento, no decidir de forma nativa, no hacer trampas. Comprobarlo tampoco es barato: una compilación

2:29 desde cero tardó cinco horas y media en 96 núcleos y 153 gigabytes de RAM, y los nombres de los teoremas son generados por máquina, por lo que el repositorio se describe a sí mismo como escrito para ser verificado en lugar de leído, que es también cómo describiría el Java empresarial. Ahora la contradicción. La publicación de Anthropic dice que Lean demuestra la corrección más allá de toda duda. Kevin Buzzard, el hombre al que le ganaron, compiló el repositorio en una máquina de 500 gigabytes que Anthropic le prestó, confirmó que se verifica, y luego escribió,

2:56 cita, matemáticamente este trabajo no nos dice esencialmente nada. Ya estaba 99,9 por ciento seguro de que el teorema era cierto, y la prueba no añade matemáticas nuevas; lo que muestra es lo que la autoformalización puede hacer ahora, y esa parte le entusiasma genuinamente. Le dieron un millón de libras durante cinco años; Anthropic tardó once días, y un cálculo aproximado de un comentarista sitúa seis mil millones de tokens de salida a precio de lista alrededor de 300.000 dólares, así que la máquina era más barata, a menos que cuentes el entrenamiento de la máquina, lo cual nadie hace.

3:24 El mejor detalle: el correo electrónico llegó mientras él estaba en un festival de música en Gales con una barra de 4G, de un nombre que nunca había oído, así que lo ignoró como una broma y lo leyó una semana después, que es la respuesta correcta a cualquier línea de asunto que contenga formalización de extremo a extremo. Mientras tanto, los humanos se recuperaron. Shin Jin-seo, el número uno del mundo en Go, venció a KataGo, el motor de Go de código abierto más potente, dos juegos a uno en Seúl con un hándicap de dos piedras, aproximadamente la diferencia entre un profesional de élite y un profesional novato.

3:50 El decisivo fue una victoria de 11,5 puntos en 221 movimientos, manteniendo una probabilidad de victoria del 99 por ciento desde la mitad de la partida, y se llevó a casa 250 millones de wones, unos 170.000 dólares, más un Genesis G90, por lo que la recompensa por derrotar a una IA sobrehumana es 170 veces la recompensa de Google por un escape del sandbox de Chrome. Su explicación: al principio copió movimientos de IA y perdió; ganó construyendo el tablero a su propio estilo, que es el consejo más útil sobre IA que he oído en todo el año, y vino de un juego de mesa. Dos líneas más en el diff.

4:22 El compilador Rust React de oxc es ahora nativo en Vite detrás de una bandera; una base de código de 1.036 archivos pasó de 14,3 segundos a 0,81 en el paso de compilación, principalmente eliminando Babel de package.json, que también es mi rutina de cuidado de la piel. E IBM lanzó a Bob, un compañero de codificación de IA que te saluda con "Hola, soy Bob", genera subagentes, moderniza código de mainframe, y envía un producto de análisis llamado Bobalytics, por lo que en algún lugar un banco está muy emocionado y nadie leyó la licencia.

4:51 Es mucho margen para un viernes; si prefieres leer esto antes que oírme decirlo, el diff llega a tu bandeja de entrada cada mañana — gratis en the daily diff dot dev, enlace abajo. Así que, el veredicto de hoy: SHIP IT. El kernel dice sí, Buzzard dice sí, las matemáticas no cambiaron, pero la forma en que comprobamos las matemáticas sí cambió. Ese es el diff de hoy. Soy Niko de Axrisi.

5:09 Fusionen con responsabilidad.

Fuentes

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