Claude probó a Fermat en 11 días. Veredicto: ENVIAR.

Lo que cubre este video

• Claude formaliza el Último Teorema de Fermat en Lean 4
• RCE en sandbox de Chromium (CVE-2026-85046), explotado en la naturaleza, 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 son 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 las diez o las 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 en la naturaleza, 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 pagará a Quad9 para que lo haga en su lugar, y esta mañana el compilador de Rust React 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 por dos. En este video: qué probó Claude realmente, 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 este es The Daily Diff. Último Teorema de Fermat: ningún número entero positivo a, b, c satisface a elevado a la n más b elevado a la n igual a c elevado a la n para cualquier n mayor que 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 erróneas en su primer año, y Andrew Wiles finalmente lo consiguió en 1995, en 129 páginas que tardaron meses en verificar los árbitros. 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 plano solo tiene 86 páginas. El investigador de Anthropic, Tianyi Peng, apuntó a docenas de agentes de Claude 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 las primeras

2:00 enjambres perdieron el rastro de quién estaba probando qué, que es lo que sucede cuando su capa de orquestación es regex 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 nativamente, no hacer trampa. Verificarlo tampoco es barato: una compilación

2:29 desde cero tomó 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 también es como 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 funciona, 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 nuevas matemáticas; lo que muestra es lo que la autoformalización puede hacer ahora, y esa parte le entusiasma genuinamente. Se le dio un millón de libras durante cinco años; Anthropic tardó once días, y el cálculo aproximado de un comentarista sitúa seis mil millones de tokens de salida al precio de lista alrededor de 300,000 dólares, por lo que la máquina era más barata, a menos que cuentes con el entrenamiento de la máquina, lo cual nadie hace.

3:24 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 del que nunca había oído hablar, así que lo descartó como una broma y lo leyó una semana después, que es la respuesta correcta a cualquier 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 La decisión fue una victoria de 11.5 puntos en 221 movimientos, manteniendo una probabilidad de victoria del 99 por ciento desde la mitad del juego, y se llevó a casa 250 millones de wones, aproximadamente 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 de sandbox de Chrome. Su explicación: al principio copió los movimientos de la IA y perdió; ganó al construir el tablero a su propio estilo, que es el consejo más útil sobre IA que he escuchado 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 ahora es 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ó Bob, un compañero de codificación de IA que te saluda con Hola, soy Bob, genera subagentes, moderniza el código del mainframe, y envía un producto de análisis llamado Bobalytics, así que en algún lugar un banco está muy emocionado y nadie leyó la licencia.

4:51 Eso es mucho margen para un viernes; si prefieres leer esto que escucharme decirlo, The Daily Diff llega a tu bandeja de entrada todas las mañanas, gratis en TheDailyDiff.dev, enlace abajo. Entonces, el veredicto de hoy: SHIP IT. El kernel dice sí, Buzzard dice sí, las matemáticas no cambiaron, pero la forma en que revisamos las matemáticas sí cambió. Esa es The Daily Diff de hoy. Soy Niko de Axrisi.

5:09 Fusiona responsablemente.

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