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

Ce que cette vidéo couvre

• Claude formalise le dernier théorème de Fermat en Lean 4
• RCE de bac à sable Chromium (CVE-2026-85046), exploitée en situation réelle, 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 contrôlés par YouTube.

0:00 Fermat a dit que sa preuve merveilleuse 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à vrai. Il était dix à onze heures à Tbilissi quand Anthropic a posté, donc naturellement j'étais éveillé. Hier, Google a lancé Chrome 152 avec douze correctifs de sécurité, l'un d'eux étant un bug V8 déjà exploité en situation réelle, et a payé au rapporteur mille dollars, ce qui est moins que la berline dont nous parlerons plus tard.

0:26 Hier également, Mullvad a annoncé la fermeture de son DNS public chiffré le 2 novembre et a payé Quad9 pour le faire à sa 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. Puis 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 fort sur Terre, donc 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 ça ne change rien et est néanmoins ravi, et comment un humain a battu la machine au Go. Nous sommes le vendredi 4 septembre, et voici The Daily Diff. Le 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 à fermer un ticket avec « ça fonctionne sur ma machine ». Un prix de 100 000 marks d'or en 1908 a attiré 621

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

2:00 nuées perdaient 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 indiquait 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, donc le dépôt se décrit comme é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 correction 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 vérifie, puis a écrit,

2:56 je cite, mathématiquement, ce travail ne nous dit pratiquement rien. Il était déjà sûr à 99,9 pour cent 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 l'enthousiasme vraiment. On lui a donné un million de livres sur cinq ans ; Anthropic a pris onze jours, et le calcul approximatif d'un commentateur place 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 : le courriel est arrivé alors qu'il était à un festival de musique au Pays de Galles avec une barre de 4G, d'un nom qu'il n'avait jamais entendu, alors il l'a considéré comme une blague et l'a lu une semaine plus tard, ce qui est la bonne réponse à toute ligne d'objet contenant une 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, soit à peu près l'écart entre un professionnel de haut niveau et un professionnel débutant.

3:50 La décision s'est faite par 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 récompense pour avoir battu une IA surhumaine est 170 fois la récompense de Google pour une évasion de sandbox Chrome. Son explication : au début, il a copié les coups de l'IA et a perdu ; il a gagné en construisant le plateau à sa manière, ce qui est le conseil le plus utile sur l'IA que j'aie entendu cette année, et il venait d'un jeu de société. Deux lignes de plus dans le The Daily 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 accueille avec « Salut, je suis Bob », génère des sous-agents, modernise le code des mainframes, et livre un produit d'analyse appelé Bobalytics, donc quelque part une banque est très enthousiaste 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 The Daily Diff arrive dans votre boîte de réception tous les matins — gratuit à The Daily Diff dot dev, lien ci-dessous. Donc, le verdict d'aujourd'hui : SHIP IT. Le noyau dit oui, Buzzard dit oui, les maths n'ont pas changé, mais la façon dont nous vérifions les maths vient de changer. C'est le The Daily 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