L’IA accélère les mathématiques, mais les humains doivent encore comprendre les preuves

Dans l’entretien du 12 septembre 2026, Steven Strogatz a décrit comment l’IA transforme la compréhension des preuves et l’identité professionnelle des mathématiciens. Le 8 septembre 2026, OpenAI a annoncé un résultat concernant une singularité en temps fini dans les équations de Navier–Stokes forcées, tridimensionnelles et incompressibles. Le 4 septembre, Anthropic avait annoncé que Claude avait formalisé dans Lean une preuve existante du dernier théorème de Fermat. Ces deux annonces relèvent donc de percées mathématiques assistées par l’IA, mais elles ne désignent pas la même chose : l’une présente une construction dont la portée doit encore être examinée par les mathématiciens, l’autre transforme une preuve déjà établie en objet formel vérifiable par ordinateur.

Cette nuance est au cœur des inquiétudes de Steven Strogatz. Le mathématicien estime que l’IA accélère la recherche tout en fragilisant les repères traditionnels du métier : être le premier, comprendre une démonstration et repousser soi-même la frontière des connaissances.

Deux avancées qui ne désignent pas la même chose

Une découverte mathématique, une formalisation et une vérification informatique sont trois opérations différentes. Les confondre produit des titres spectaculaires, mais brouille rapidement la réalité scientifique.

La différence est simple à retenir : Claude n’a pas découvert le dernier théorème de Fermat. Anthropic a décrit la formalisation, dans Lean, d’une preuve existante associée aux travaux d’Andrew Wiles et de Richard Taylor.

Ce qu’OpenAI a affirmé sur Navier–Stokes

OpenAI a décrit une preuve analytique et une formalisation dans Lean portant sur une singularité en temps fini : dans les conditions étudiées, la vitesse pourrait devenir non bornée. Le cadre annoncé concerne les équations de Navier–Stokes forcées, en trois dimensions et pour un fluide incompressible.

Le problème d’existence et de régularité de Navier–Stokes fait partie des sept problèmes du prix du millénaire du Clay Mathematics Institute. Chacun est associé à une récompense d’un million de dollars. Mais une annonce d’entreprise et un artefact Lean ne suffisent pas, à eux seuls, à transformer un résultat en solution mathématique acceptée.

La réponse à la question la plus importante est donc non : cette annonce ne signifie pas que le problème du millénaire est résolu au sens reconnu par la communauté mathématique. Il faut encore que les spécialistes examinent la construction, sa portée exacte et ses hypothèses avant de lui attribuer cette portée.

Le problème n’est pas seulement de vérifier si des lignes de code s’exécutent correctement. Il faut aussi établir que le bon problème a été encodé et que la démonstration répond bien à la question mathématique posée.

Ce que Claude a fait avec la preuve de Fermat

Le projet présenté par Anthropic est spectaculaire par son ampleur, mais sa nouveauté est d’une autre nature. Claude a formalisé une preuve déjà connue du dernier théorème de Fermat dans Lean. Anthropic a indiqué que le travail avait produit environ 29 500 théorèmes intermédiaires utilisés dans la démonstration finale.

Autrement dit, l’IA n’a pas trouvé un nouveau théorème. Elle a contribué à convertir une preuve mathématique existante en une forme suffisamment précise pour être traitée par un assistant de preuve.

Cette opération a une valeur propre. Une formalisation oblige à expliciter les définitions, les dépendances et les hypothèses qu’une démonstration destinée à des humains peut parfois laisser implicites. Elle ne remplace toutefois pas l’histoire de la découverte ni le raisonnement qui a conduit à la preuve originale.

Ce que Lean vérifie réellement

Lean est un assistant de preuve. Il vérifie mécaniquement que les étapes écrites dans un développement formel suivent les définitions, les axiomes et les hypothèses qui y sont encodés.

C’est une garantie importante, mais ciblée. Lean peut confirmer que les étapes formalisées s’enchaînent correctement dans le système choisi. Il ne décide pas seul si le développement formalise le problème que les chercheurs pensaient traiter, si les hypothèses correspondent à l’intention mathématique ou si le résultat mérite une reconnaissance générale.

Cette distinction explique pourquoi une formalisation ne clôt pas automatiquement le débat. La machine contrôle la cohérence des étapes codées ; les mathématiciens doivent encore comprendre la construction, en évaluer la portée et déterminer ce qu’elle apporte réellement.

Le métier de mathématicien sous pression

Pour Steven Strogatz, le travail humain ne disparaît pas simplement parce qu’une machine produit ou formalise des arguments. Il change de centre de gravité. Il parle de « digestion des preuves » : expliquer une démonstration dans des termes que les humains peuvent comprendre et apprécier.

Selon lui, les experts humains restent actuellement les mieux placés pour accomplir cette tâche. Ils doivent relier les symboles à une idée, repérer les hypothèses décisives et juger l’importance du résultat. Cette fonction d’interprétation est moins visible qu’une démonstration produite en quelques heures, mais elle détermine la manière dont la communauté peut réellement utiliser cette démonstration.

Alex Townsend décrit une tension comparable dans son propre travail. Après quinze ans consacrés aux mathématiques de recherche, il a dit se sentir menacé par un système capable de dépasser ce qu’il considérait comme son niveau de pointe. Dans le même temps, l’IA peut rendre abordables des travaux qui semblaient auparavant trop difficiles ou trop longs.

Le paradoxe est là : l’outil peut augmenter la capacité de recherche tout en diminuant, pour certains chercheurs, le sentiment d’être eux-mêmes à la frontière du savoir. Strogatz résume cette inquiétude en affirmant que les mathématiques pures pourraient être « dévastées ou révolutionnées », selon le point de vue adopté.

Ce qui compte désormais

Pour juger une future annonce mathématique produite avec l’IA, quatre questions sont plus utiles qu’un simple compteur d’agents ou de lignes de code :

• Quel problème précis est traité ? Les équations, les dimensions, les forces et les hypothèses doivent être clairement définies.
• S’agit-il d’une découverte ou d’une formalisation ? Encoder une preuve existante n’est pas découvrir le théorème qu’elle démontre.
• Que vérifie exactement le système formel ? Lean contrôle les étapes et les hypothèses qui lui sont données ; il ne remplace pas l’examen de la portée mathématique.
• La communauté peut-elle comprendre et évaluer le résultat ? Une démonstration doit être reconstruite, expliquée et examinée avant de modifier durablement l’état des connaissances.

L’IA est donc déjà un accélérateur et un outil de formalisation pour les mathématiques. Mais la prochaine frontière ne sera pas seulement de produire davantage de preuves. Elle consistera à les rendre compréhensibles, à préserver la responsabilité intellectuelle de ceux qui les évaluent et à décider ce que signifie encore « faire » des mathématiques lorsque la machine participe à chaque étape.