Actualité : Aucun humain n'avait déchiffré ce casse-tête mathématique, l'IA l'a fait en trois jours

En 2014, le mathématicien Dan Anderson a posé une conjecture d'algèbre irrésolue. L'outil chinois l'a craquée en 80 heures. Soit un peu plus de trois jours, sans intervention humaine sur les choix mathématiques. Le travail a été publié sur arXiv. Mais il est important de préciser que le papier n'a pas été validé par les pairs pour le moment.

Le projet est piloté par quinze chercheurs de l'université de Pékin. Sauf que voilà, le coup d'éclat tient moins à la prouesse de calcul qu'à la méthode. L'architecture repose sur deux agents d'IA qui se répartissent le travail.

Le premier, appelé Rethlas, joue le rôle de chercheur. Il explore des pistes de démonstration comme le ferait un mathématicien humain. Rethlas s'appuie sur un moteur de recherche spécialisé, Matlas, qui fouille des décennies de littérature mathématique pour trouver des théorèmes utiles. En gros, il reproduit la démarche d'un universitaire face à un problème ouvert.

Le second agent s'appelle Archon. Son travail consiste à transformer les pistes de Rethlas en démonstrations formelles vérifiables. Archon utilise un autre moteur de recherche, LeanSearch, qui pioche dans la bibliothèque Mathlib de Lean 4. Lean 4 est un langage de programmation qui sert à la vérification automatique des preuves mathématiques. Sa bibliothèque rassemble des centaines de milliers de théorèmes et de définitions maintenus par une communauté mondiale. Archon traduit une preuve informelle en projet Lean 4 complet, avec tout ce qui encadre la démonstration finale.

Le problème en question n'est pas une énigme médiatique. Il a été posé en 2014 par Dan Anderson, ancien professeur à l'université de l'Iowa, mort en 2022 à l'âge de 73 ans. Son problème porte sur une branche assez technique de l'algèbre. En gros, il voulait savoir si une propriété mathématique en implique toujours une autre pour certains objets bien précis.

Le duo d'IA chinois a apporté une réponse négative. Il a construit un contre-exemple, c'est-à-dire un cas particulier qui invalide l'idée de départ. La démonstration a été formalisée et vérifiée par Lean 4 en 80 heures de calcul.

Et pour cause, les preuves mathématiques exigent une rigueur totale. Même les démonstrations rédigées par des experts humains renferment parfois des erreurs discrètes. Les preuves produites par les grands modèles de langage sont encore moins fiables. Les hallucinations restent un problème de ces outils.

OpenAI et Google sont aussi dans la course

Le cas chinois comble ce fossé avec deux agents, un de raisonnement et un de vérification. En clair, l'IA raisonne et prouve elle-même que son raisonnement tient debout. Le code source de Rethlas et d'Archon a été publié sur GitHub sous le nom de FrenzyMath. Résultat, n'importe quelle équipe a accès à la méthode pour la tester sur d'autres problèmes ouverts.

La concurrence sur ce terrain monte rapidement. En début d'année 2026, Aletheia de Google DeepMind a résolu quatre problèmes ouverts d'une base de conjectures du grand mathématicien hongrois Paul Erdős. OpenAI a aussi montré des capacités de preuves formelles. Mais ces deux cadres exigeaient encore une supervision humaine sur les étapes clés. L'équipe de Pékin revendique la suppression presque totale de cette supervision.

Mais ce n'est pas tout. Les chercheurs eux-mêmes nuancent leur victoire. Le problème posé par Dan Anderson reste obscur pour le grand public. Il ne joue pas dans la même cour que l'hypothèse de Riemann ou le problème P contre NP. Des grandes énigmes pour lesquelles la fondation Clay promet un million de dollars à qui les résoudra.

Rien ne garantit non plus que la méthode fonctionnera sur des problèmes plus ardus. Pour autant, dans une discipline qui résiste à l'automatisation depuis des siècles, ce résultat marque une étape. L'équipe précise qu'un mathématicien humain accélère encore le processus quand il intervient pour orienter Archon. Les chercheurs voient dans leurs résultats un exemple concret d'une recherche mathématique qui s'automatise grâce à l'IA.