Imperial College de Londres

Le 4 septembre 2026, Anthropic a mis en ligne sous licence Apache 2.0 un dépôt contenant une preuve complète du dernier théorème de Fermat en Lean 4, vérifiée par machine. Le dépôt compte 60 475 modules, 29 511 théorèmes et 1 450 modules de définitions, et aucun n'utilise sorry, axiom ni native_decide. Le noyau Lean 4.33.1 valide l'ensemble, l'outil comparator v4.33.0 confirme que l'énoncé prouvé est bien celui de Mathlib, et nanoda 0.4.13, un second noyau écrit en Rust, a accepté 1 052 234 déclarations sans erreur. Anthropic présente ce dépôt comme un artefact de recherche non maintenu. Les sources Lean ont été produites par des agents d'IA à partir de code écrit à la main : 106 fichiers reprennent le projet FLT de l'Imperial College London dirigé par Kevin Buzzard et le projet flt-regular.

Le 19 mai 2026, Google DeepMind a publié dans Nature l'article Accelerating scientific discovery with Co-Scientist, décrivant un système multi-agents bâti sur Gemini qui génère, débat et fait évoluer des hypothèses scientifiques. L'architecture repose sur des agents qui produisent, critiquent et affinent itérativement les hypothèses, avec un cadre d'exécution asynchrone et un processus d'évolution par tournoi. La validation a porté sur trois applications biomédicales : le repositionnement de médicaments, la découverte de nouvelles cibles et l'explication de mécanismes de résistance aux antimicrobiens. Le système a notamment identifié des candidats au repositionnement et des combinaisons thérapeutiques pour la leucémie myéloïde aiguë, validés in vitro. Au sein de l'initiative Fleming de l'Imperial College de Londres, Co-Scientist a retrouvé des hypothèses obtenues par l'équipe après une décennie de travaux.