Un désalignement de l’IA en mathématiques : Tao, The Economist et un débat HN de 622 commentaires

Le 11 septembre 2026, le blog de Terry Tao et The Economist ont tous deux publié des articles sur le même sujet : le mauvais alignement de l'IA en mathématiques. Le fil Hacker News qui les regroupe a atteint 560 points et 622 commentaires — la discussion fait ici l'essentiel du travail, puisque les articles originaux sont payants et que les commentaires HN portent la substance technique.

Ce qui est réellement débattu

Le cadrage porte sur le mauvais alignement, pas sur la capacité. Le problème n'est pas que les LLM soient mauvais en maths — c'est que les incitations autour des mathématiques assistées par IA pointent ailleurs que vers les mathématiques. Concrètement, les types d'affirmations qui circulent dans ce débat sont :

• Pression à la formalisation : Lean 4 et Mathlib ont rendu viables les preuves vérifiables par machine, ce qui change ce que signifie « terminé ». Un LLM qui produit une esquisse de preuve plausible n'est pas la même chose qu'un LLM qui produit une preuve qui compile.
• Déplacement des benchmarks : Des outils comme AlphaProof et AlphaGeometry obtiennent des scores sur des problèmes de compétition (style IMO). C'est une cible étroite et bien spécifiée. La recherche mathématique ne l'est pas.
• Goulot de relecture : Si l'IA accélère la génération de preuves plus vite que les humains ne peuvent les vérifier, on obtient un arriéré croissant d'affirmations non vérifiées — l'inverse de ce que la formalisation est censée apporter.
• Crédit et attribution : Le cadrage de Tao porte généralement sur l'endroit où le jugement humain doit encore rester dans la boucle, et sur ce qui se passe quand ce n'est pas le cas.

Pourquoi les développeurs devraient s'y intéresser

Le schéma se généralise. Si vous avez déployé un agent qui écrit du code, vous connaissez déjà le mode de défaillance : le modèle produit quelque chose de syntaxiquement valide et sémantiquement faux, et le coût se déplace de l'écriture vers la relecture. Les mathématiques sont le cas de test le plus propre parce qu'elles disposent d'un vérificateur — Lean, Coq, Isabelle — qui ne se soucie pas des impressions. Si le mauvais alignement se manifeste même là, il se manifestera partout ailleurs d'abord.

Le fil HN est l'artefact utile. 622 commentaires sur une paire d'articles payants signifient généralement que les commentaires sont l'endroit où vivent les vrais arguments. Lisez-le.