Claude a prouvé Fermat en 11 jours. Verdict : SHIP IT.

Ce que couvre cette vidéo

• Claude formalise le dernier théorème de Fermat dans Lean 4
• RCE dans le bac à sable Chromium (CVE-2026-85046), exploité dans la nature, prime de 1 000 $
• Shin Jin-seo bat KataGo avec un handicap de deux pierres

Transcription traduite

Traduit de la narration originale en anglais. L'audio et les sous-titres disponibles sont gérés par YouTube.

0:00 Fermat a dit que sa merveilleuse preuve ne tiendrait pas dans la marge, et aujourd'hui Anthropic a publié la marge : treize millions de lignes de Lean, cinq fois la taille de Mathlib, prouvant un théorème que tous les mathématiciens croyaient déjà. Il était dix heures et demie à Tbilissi quand Anthropic a posté, alors naturellement j'étais éveillé. Hier, Google a livré Chrome 152 avec douze correctifs de sécurité, dont un bug V8 déjà exploité dans la nature, et a payé le rapporteur mille dollars, ce qui est moins que la berline dont nous parlerons plus tard.

0:26 Toujours hier, Mullvad a annoncé qu'il fermerait son DNS public chiffré le 2 novembre et paierait Quad9 pour le faire à la place, et ce matin le Rust React Compiler est devenu natif dans Vite, tandis que Hacker News a découvert IBM Bob, un agent de codage IA. Ensuite, Claude a formalisé le dernier théorème de Fermat, et sur la même première page, un grand maître coréen a battu le moteur de Go le plus puissant sur Terre, alors aujourd'hui, l'humanité a fait un sur deux. Dans cette vidéo : ce que Claude a réellement prouvé, ce que cela a coûté,

0:52 pourquoi le mathématicien qui a passé sa carrière là-dessus dit que cela ne change rien et est ravi quand même, et comment un humain a battu la machine au Go. Nous sommes le vendredi 4 septembre, et voici The Daily Diff. Dernier théorème de Fermat : aucun entier positif a, b, c ne satisfait a à la puissance n plus b à la puissance n égale c à la puissance n pour tout n supérieur à 2. Fermat l'a griffonné dans une marge vers 1637 et est mort sans montrer son travail, faisant de lui le premier développeur à clore un ticket avec « fonctionne sur ma machine ». Un prix de 100 000 marks d'or en 1908 a attiré 621 preuves erronées

1:25 la première année, et Andrew Wiles l'a finalement obtenue en 1995, en 129 pages que les arbitres ont mis des mois à vérifier. Formaliser signifie réécrire cette preuve afin que Lean, un assistant de preuve, puisse vérifier chaque étape mécaniquement, et Kevin Buzzard à Imperial a mené un effort humain pour faire exactement cela depuis 2024 ; le plan seul fait 86 pages. La chercheuse d'Anthropic Tianyi Peng a dirigé des dizaines d'agents Claude vers cela à la place, sur une plateforme appelée Prove2Me qui maintient un DAG d'énoncés de théorèmes afin que les agents sachent quoi prouver ensuite, car sans cela les premières

2:00 nuées ont perdu la trace de qui prouvait quoi, ce qui arrive lorsque votre couche d'orchestration est une expression régulière avec un budget marketing. Onze jours plus tard, le nœud racine affichait PROUVÉ : treize millions de lignes de Lean, 29 500 théorèmes intermédiaires, environ six milliards de jetons de sortie d'un modèle interne à peu près comparable à Claude Fable 5.1. La construction échoue à moins que la preuve ne repose exactement sur les trois axiomes standard de Lean : non désolé, pas de décision native, pas de tricherie. La vérification n'est pas non plus bon marché : une

2:29 construction à partir de zéro a pris cinq heures et demie sur 96 cœurs et 153 gigaoctets de RAM, et les noms des théorèmes sont générés par machine, de sorte que le dépôt se décrit comme étant écrit pour être vérifié plutôt que lu, ce qui est aussi la façon dont je décrirais le Java d'entreprise. Maintenant, la contradiction. Le poste d'Anthropic dit que Lean démontre la justesse au-delà de tout doute. Kevin Buzzard, l'homme qui a été battu sur le fil, a compilé le dépôt sur une machine de 500 gigaoctets qu'Anthropic lui a prêtée, a confirmé qu'il fonctionnait, puis a écrit,

2:56 je cite, mathématiquement, ce travail ne nous dit essentiellement rien. Il était déjà sûr à 99,9 % que le théorème était vrai, et la preuve n'ajoute pas de nouvelles mathématiques ; ce qu'elle montre, c'est ce que l'autoformalisation peut faire maintenant, et cette partie le passionne vraiment. On lui a donné un million de livres sur cinq ans ; Anthropic a pris onze jours, et un calcul rapide d'un commentateur estime six milliards de jetons de sortie au prix catalogue à environ 300 000 dollars, donc la machine était moins chère, à moins de compter la formation de la machine, ce que personne ne fait.

3:24 Meilleur détail : l'e-mail est arrivé alors qu'il était à un festival de musique au Pays de Galles avec une seule barre de 4G, d'un nom qu'il n'avait jamais entendu, alors il l'a considéré comme un canular et l'a lu une semaine plus tard, ce qui est la bonne réponse à toute ligne d'objet contenant « formalisation de bout en bout ». Pendant ce temps, les humains ont repris le dessus. Shin Jin-seo, le numéro un mondial de Go, a battu KataGo, le moteur de Go open-source le plus puissant, deux parties à une à Séoul avec un handicap de deux pierres, environ l'écart entre un professionnel de haut niveau et un professionnel débutant.

3:50 Le match décisif fut une victoire de 11,5 points en 221 coups, conservant une probabilité de victoire de 99 % à partir du milieu de partie, et il a remporté 250 millions de wons, environ 170 000 dollars, plus une Genesis G90, donc la prime pour battre une IA surhumaine est 170 fois la prime de Google pour une évasion de bac à sable Chrome. Son explication : au début, il a copié les mouvements de l'IA et a perdu ; il a gagné en construisant le plateau dans son propre style, ce qui est le conseil le plus utile sur l'IA que j'ai entendu de l'année, et il est venu d'un jeu de société. Deux lignes de plus dans le diff.

4:22 Le compilateur Rust React d'oxc est maintenant natif dans Vite derrière un seul drapeau ; une base de code de 1 036 fichiers est passée de 14,3 secondes à 0,81 dans l'étape de compilation, principalement en supprimant Babel de package.json, ce qui est aussi ma routine de soins de la peau. Et IBM a lancé Bob, un partenaire de codage IA qui vous salue par « Salut, je suis Bob » , génère des sous-agents, modernise le code mainframe, et livre un produit d'analyse appelé Bobalytics, donc quelque part une banque est très enthousiasmée et personne n'a lu la licence.

4:51 C'est beaucoup de marge pour un vendredi ; si vous préférez lire ceci plutôt que de m'entendre le dire, le diff atterrit dans votre boîte de réception chaque matin — gratuit sur the daily diff dot dev, lien ci-dessous. Alors, verdict du jour : SHIP IT. Le noyau dit oui, Buzzard dit oui, les mathématiques n'ont pas changé, mais la façon dont nous vérifions les mathématiques vient de le faire. C'est le diff d'aujourd'hui. Je suis Niko d'Axrisi.

5:09 Fusionnez de manière responsable.

Sources

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