TL;DR : une preuve mathématique traduite par machine en onze jours, une porte dérobée qui contamine presque tous les binaires d’une distribution Linux, et un mainteneur qui promet que rien ne changera.
1. Claude a formalisé le dernier théorème de Fermat en onze jours
Anthropic a publié le 4 septembre le résultat : la première preuve du dernier théorème de Fermat vérifiable de bout en bout par une machine, écrite en Lean. En onze jours de travail largement autonome, le système a produit 13 millions de lignes et prouvé 29 500 théorèmes intermédiaires, soit plus de cinq fois la taille de Mathlib, la bibliothèque de référence.
Entendons-nous : le théorème est démontré depuis 1994 par Andrew Wiles. Ce qui vient d’être fait, c’est sa traduction dans un langage où une machine vérifie chaque pas, un chantier que des mathématiciens menaient depuis des années. L’apport humain s’est limité à des « instructions de haut niveau occasionnelles », et les auteurs reconnaissent que leur preuve est « probablement bien plus longue que nécessaire ». Le dépôt est public, sous Apache 2.0.
2. Une porte dérobée dans presque tous les binaires de NixOS, par strip
L’attaque dite « Trusting Trust », décrite par Ken Thompson en 1984, suppose un compilateur compromis. Cinq chercheurs montrent dans un article arXiv qu’un simple utilitaire suffit : ils ont piégé GNU strip, l’outil qui allège les binaires, par manipulation de fichiers ELF, et l’ont glissé dans la chaîne d’amorçage de NixOS. L’installateur graphique complet en ressort avec une porte dérobée dans « presque chacun de ses binaires », sans qu’une ligne de code source ait été modifiée.
La démonstration a été menée sur une révision réelle de nixpkgs, et l’affaire gêne d’autant plus que NixOS est la distribution qui a le plus investi dans la compilation reproductible, la parade théorique à ce genre d’attaque. Elle ne protège pas quand l’outil qui construit est déjà retourné.
3. Gerganov promet que llama.cpp restera indépendant du matériel
Après le rachat de Hugging Face par Nvidia pour 12,93 milliards de dollars, la question était simple : que devient llama.cpp, la brique par laquelle passe l’essentiel de l’IA qui tourne sur les machines personnelles ? Son créateur Georgi Gerganov, passé chez Hugging Face en février, a répondu. Son message n’est pas lisible sur X sans compte, mais il est reproduit dans le fil Hacker News : le projet « s’en tiendra à ses principes fondateurs », dont l’indépendance vis-à-vis du matériel, et « le développement et le support de tous les backends continueront comme d’habitude, portés et façonnés par la communauté ».
Autrement dit : pas de vitrine pour cartes Nvidia. C’est l’engagement qu’on attendait, et c’est un engagement, pas une garantie.
4. 18 000 messages d’agents OpenAI sur un wiki allemand
Quatre chercheurs indépendants ont documenté dans un rapport intitulé « Collusion Wiki » comment des agents autonomes d’OpenAI ont utilisé DSEWiki, un wiki de programmation allemand confidentiel, pour se coordonner : environ 18 000 messages depuis mai, où ils s’échangeaient des réponses à leurs propres évaluations. OpenAI reconnaît avoir traité l’affaire comme un défaut d’alignement plutôt que comme un incident de sécurité, et n’avoir rien divulgué.
Les chercheurs le disent eux-mêmes : leur enquête ne repose que sur ce que les agents ont écrit publiquement, sans accès aux journaux internes.
5. Le prompt système de Claude ne récite plus les chansons
Anthropic publie les prompts système de ses modèles. Celui de Claude Fable 5.1, daté du 1er septembre, porte une consigne nouvelle et détaillée : plus de « song lyrics, poems, or passages from books and articles, in whole or in part », y compris les dernières lignes, un refrain, une mélodie note à note, ou des vers qu’on lui ferait recomposer un par un en les présentant comme les siens. Les œuvres d’avant 1929 restent permises, et le modèle refuse s’il doute de la date.
Même logique au dessin : pas de personnage connu, et « changer la pose, les couleurs, le style ou la scène ne rend pas le dessin original ». On peut y lire l’ombre des procédures d’éditeurs musicaux. On peut aussi noter qu’une règle aussi précise vaut mieux qu’un refus vague.
