La lettre Intelligences — #10 : Laboratoires robotisés, preuves formelles et travail en mutation

Bonjour,

La journée fait apparaître deux mouvements complémentaires : l’IA s’attaque à des problèmes scientifiques d’une ampleur exceptionnelle, mais la valeur de ces résultats dépend plus que jamais de preuves vérifiables, de relectures indépendantes et d’un retour au monde physique. Dans les laboratoires comme dans les entreprises, l’automatisation ne supprime ni le contrôle humain ni les arbitrages économiques.

À la une — Une hypothèse centrale de l’informatique théorique remise en cause

OpenAI affirme que ses modèles ont réfuté l’Exponential Time Hypothesis (ETH), une conjecture formulée à la fin des années 1990 selon laquelle certains problèmes de satisfaisabilité ne peuvent pas être résolus en temps sous-exponentiel. Le résultat annoncé porte sur le comptage exact des solutions de formules booléennes et a été formalisé dans l’assistant de preuve Lean.

L’entreprise a confié l’examen du résultat à un groupe conduit par Russell Impagliazzo et Ramamohan Paturi, deux des auteurs de l’hypothèse, ainsi que Ryan Williams, spécialiste de la complexité au MIT. Leur participation ne vaut pas validation : les données brutes et la preuve ont été rendues publiques pour permettre une vérification collective.

Anthropic a publié presque simultanément une autre démonstration attribuée à un modèle de recherche interne de Claude. Son dépôt précise que le résultat est purement asymptotique : il ne fournit pas, à ce stade, une méthode pratique pour résoudre de grandes formules, ne tranche pas P contre NP et doit encore être confronté à une lecture humaine de l’énoncé formalisé.

Pourquoi cela compte. Si l’une de ces démonstrations résiste à l’examen, des centaines de résultats conditionnels fondés sur ETH devront être relus. Mais l’épisode montre surtout une nouvelle organisation de la recherche : un modèle produit une conjecture ou une preuve, un vérificateur contrôle la syntaxe logique, puis des experts doivent établir que le théorème formalisé correspond bien à l’affirmation scientifique.

Lire l’annonce scientifique et le dispositif de vérification d’OpenAI ; examiner la formalisation publiée par Anthropic.

Mathématiques — Le « théorème énorme » tient dans 43,1 millions de lignes Lean

Axiom annonce avoir formalisé la classification des groupes simples finis, l’un des plus vastes édifices des mathématiques modernes. La démonstration historique occupe environ 15 000 pages, réparties dans plus de 500 articles rédigés par une centaine de mathématiciens. Le projet Lean totalise 43,1 millions de lignes et environ 2,05 millions de déclarations.

Des essaims d’agents ont travaillé pendant vingt-quatre jours à partir d’une carte de dépendances construite sur la littérature publiée. L’intérêt ne réside pas seulement dans la taille : le noyau de Lean peut vérifier chaque étape sans faire confiance au modèle qui l’a rédigée. L’équipe dit également avoir rencontré un problème dans un argument publié du théorème du groupe déséquilibré et avoir emprunté une voie alternative.

Pourquoi cela compte. Une formalisation complète transforme une preuve dispersée, difficile à parcourir et parfois dépendante d’arguments anciens en un objet testable. Elle ne remplace pas l’explication mathématique, mais elle rend les dépendances, les hypothèses et les éventuelles lacunes beaucoup plus visibles.

Lire le récit technique d’Axiom et explorer la carte de la preuve formalisée.

Chimie — 215 millions de dollars pour relier modèles, robots et molécules

Warp Sciences, fondée notamment par Kevin Weil, ancien responsable produit et science d’OpenAI, est sortie de la discrétion avec 215 millions de dollars de financement. Son objectif est de construire aux États-Unis des laboratoires de chimie où des chercheurs, des modèles et des robots fabriquent puis testent les molécules nécessaires à la découverte de médicaments.

Le premier service porte sur la synthèse d’analogues pendant l’optimisation de candidats-médicaments. L’entreprise veut créer une boucle où les expériences physiques génèrent des données, où ces données améliorent les modèles et où les modèles proposent de nouvelles expériences. La valorisation de 865 millions de dollars rapportée par la presse reste un indicateur financier, pas la preuve que cette boucle scientifique fonctionne déjà à l’échelle industrielle.

Piste pratique. Pour évaluer ce type de laboratoire, il faudra suivre le délai entre conception et test, le taux d’expériences reproductibles, le coût par composé utile et la part des résultats négatifs réellement réinjectée dans les modèles.

Consulter l’annonce de Warp Sciences et la composition de l’équipe.

Les informations à retenir

Microsoft ouvre une porte de sortie volontaire à 60 000 salariés

Microsoft propose une offre de départ volontaire à environ 60 000 personnes, soit près de 27 % de ses 223 000 salariés. Le programme concerne certains employés jusqu’au niveau 70 aux États-Unis, au Canada, au Royaume-Uni et en Inde ; les participants doivent se décider en décembre et quitteraient l’entreprise le 31 décembre.

La direction présente la mesure comme une manière de donner davantage de choix pendant une période de transformation. Le contexte est néanmoins celui d’investissements massifs dans les infrastructures d’IA. L’offre ne permet pas, à elle seule, d’attribuer chaque départ à l’automatisation : elle traduit aussi une recherche de flexibilité et de maîtrise des coûts.

Lire les éléments confirmés sur le programme de départs volontaires.

Cinéma — Une première entièrement générée par IA ne trouve pas encore son public

Sanxingdui: Future Past, présenté par ses producteurs comme le premier long métrage chinois entièrement généré par IA à bénéficier d’une sortie en salles, n’avait engrangé qu’environ 1,21 million de yuans après son lancement du 23 octobre. Sa production aurait coûté plus de 10 millions de yuans et mobilisé près de cent personnes pendant plus de deux ans.

Le contre-exemple est instructif : l’usage massif de l’IA n’a ni supprimé la durée de production ni garanti l’intérêt du public. Quelques jours d’exploitation ne suffisent pas à établir un verdict définitif, mais ils rappellent qu’une prouesse technique ne se transforme pas automatiquement en désir de cinéma.

Consulter les chiffres de production et de fréquentation disponibles.

Recherche biomédicale — Claude entre dans six partenariats de développement

Anthropic indique travailler avec six organisations du médicament, dont Bristol Myers Squibb, Enveda et Generate Biomedicines, tout en lançant ses propres programmes exploratoires. Les travaux annoncés restent pour l’essentiel précliniques : ils concernent la conception, l’analyse et la sélection de pistes, pas des traitements déjà validés chez l’humain.

L’entreprise évoque notamment plus de cent anticorps bispécifiques en cours de test cellulaire dans deux programmes sur des maladies pédiatriques rares. Les échéances avancées pour sélectionner des candidats en 2027 et envisager des essais à partir de 2028 sont des objectifs, non des engagements cliniques.

Lire le bilan préclinique et les limites présentés par Anthropic.

Le chiffre

43,1 millions. C’est le nombre de lignes Lean annoncées pour la formalisation de la classification des groupes simples finis. Ce volume ne mesure pas à lui seul la qualité mathématique, mais il donne l’échelle d’un passage inédit : de milliers de pages humaines à une chaîne logique que le noyau d’un assistant de preuve peut contrôler.

Pour approfondir dans notre réseau

• Pourquoi l’intelligence artificielle pourrait fragiliser la méthode scientifique elle-même
• L’ambition industrielle des robots intelligents
• Pourquoi l’intelligence artificielle ne détruit toujours pas l’emploi

Recevez La lettre Intelligences

Pour ne manquer aucune édition, inscrivez-vous à la newsletter Intelligences. Vous recevrez directement nos prochaines veilles sur l’intelligence artificielle, la recherche, les usages et leurs conséquences.

La rédaction d’Intelligences

Merci de votre lecture. À très bientôt pour une nouvelle édition de La lettre Intelligences.