Navier-Stokes par l'IA : les preuves mathématiques sont-elles

Les systèmes d'intelligence artificielle les plus avancés peuvent-ils produire des preuves mathématiques truquées, sans que personne ne s'en aperçoive ? Le Monde pose la question dans un article publié le 28 septembre 2026, sans trancher, mais en pointant plusieurs signaux inquiétants.

Un problème du millénaire résolu, en apparence

Le 8 septembre 2026, OpenAI a annoncé qu'un de ses modèles internes, non accessible au public, était parvenu à démontrer qu'une solution des équations de Navier-Stokes pouvait « exploser » en temps fini. Il s'agit d'une version de l'un des sept problèmes du millénaire posés par l'institut Clay, doté d'un million de dollars selon Sciences et Avenir.

Pour y parvenir, l'entreprise a mobilisé environ 10 000 agents en parallèle pendant 88 heures, aboutissant à une preuve de 165 pages, rapporte Numerama. Le texte échangé au total représenterait 2,7 millions de messages, selon Sciences et Avenir. La démonstration a ensuite été formalisée dans le langage Lean, censé garantir sa cohérence logique.

Lean, l'outil qui certifie sans expliquer

Lean et son équivalent Rocq sont des assistants de preuve utilisés depuis des années pour certifier des logiciels critiques en aéronautique ou en énergie, rappelle Le Monde. Les géants du numérique s'en servent désormais pour entraîner leurs modèles et vérifier leurs réponses mathématiques.

Mais cette formalisation n'est pas neutre. Yannick Forster, chercheur à l'Institut national de recherche en sciences et technologies du numérique, résume le glissement en cours.

« Nos outils étaient une niche. Maintenant ils sont à la mode… mais on oublie leur nom », Yannick Forster, chercheur à l'Institut national de recherche en sciences et technologies du numérique.

Patrick Massot, professeur au Laboratoire de mathématiques d'Orsay de l'université Paris-Saclay, va plus loin. Il rappelle que ces outils ont été conçus pour aider des chercheurs à comprendre pourquoi un résultat est vrai, pas seulement pour le certifier mécaniquement.

« Ces outils ont été créés pour être utilisés par des humains de bonne foi voulant vérifier de façon très poussée que tous les arguments d'une démonstration fonctionnent ensemble. Le but est de mieux comprendre pourquoi un résultat est vrai et comment les idées interagissent. Cela va très au-delà de la certification que le résultat est vrai. Mais les utilisateurs d'IA réduisent désormais l'activité de formalisation à cette certification », Patrick Massot, professeur au Laboratoire de mathématiques d'Orsay, université Paris-Saclay.

Un exemple illustre l'ampleur du problème : la démonstration du théorème de Fermat par IA a nécessité 13 millions de lignes de code Lean, un volume qu'aucun humain n'aurait pu vérifier ligne par ligne, selon Le Monde.

Des mathématiciens alertent sur une indigestion de preuves

Le mathématicien Terence Tao a averti la Silicon Valley contre le triomphalisme, notamment après des annonces spectaculaires sur l'hypothèse de Riemann, rapporte Numerama. Il distingue cinq étapes entre la preuve brute générée par IA et le chapitre de manuel scolaire, la dernière étant la validation par la communauté.

« Si les auteurs ne parviennent pas à démontrer de manière convaincante qu'ils sont capables de présenter leurs résultats lors d'une intervention claire, de niveau expert, exacte et citant correctement leurs sources, alors ces résultats ne devraient pas être publiés », Terence Tao, mathématicien.

Des mathématiciens de Cambridge, Oxford, Columbia et ETH Zurich ont publié un texte de onze pages sur les risques que l'IA fait peser sur leur discipline, selon Clubic. Ils estiment qu'un système peut produire un argument qui ressemble à une preuve sans qu'on puisse vérifier qu'il est correct.

Sur son blog, le chercheur David Monniaux évoque un « séisme » et pointe un problème concret : les experts humains sont submergés par des démonstrations générées par IA, dont beaucoup s'avèrent inutilisables, faute de temps pour toutes les vérifier.

Des accusations de plagiat et un accord encore lointain

L'annonce d'OpenAI n'a pas fait l'unanimité. Numerama rapporte des accusations de plagiat visant le groupe, sans que la preuve ait pour l'instant reçu l'acceptation de la communauté mathématique. Amaury Hayat, cité par La Libre, signale que des chercheurs soumettent déjà à des revues des articles entièrement rédigés par IA, sans les comprendre eux-mêmes.

Antoine Chambert-Loir, cité par Sciences et Avenir, rappelle qu'un programme de vérification « n'est jamais qu'un programme informatique », susceptible de bugs sur des démonstrations de plusieurs milliers de pages. Pour ces chercheurs, la formalisation en Lean atteste d'une cohérence logique, mais ne dispense pas d'un travail humain pour vérifier que la solution correspond bien à la question posée par l'institut Clay.