Cette IA a résolu un problème mathématique ouvert depuis 45 ans

Ce n’est pas la première fois qu’une IA s’illustre sur un problème de mathématiques réputé complexe — et ce ne sera manifestement pas la dernière. Mais, ce 11 janvier 2026, l’exercice a quelque chose de singulier : le modèle GPT 5.2 Pro a proposé une solution à un problème étudié depuis près de 45 ans. Et, preuve de sa solidité : la démonstration a été examinée et validée par Terence Tao, mathématicien austro-américain, régulièrement cité comme l’un des meilleurs au monde aujourd’hui.

En quoi consiste ce problème de maths des années 80 ?

Le problème, choisi et soumis par Neel Somani – un entrepreneur et ingénieur logiciel — est l’Erdos Problem #397. Issu de l’ouvrage Old and New Problems and Results in Combinatorial Number Theory (1980), coécrit par Paul Erdös et Ronald Graham, il porte sur les produits de coefficients binomiaux centraux. Pour résumer le plus simplement possible, l’Erdös 397 demande si les coïncidences parfaites entre produits de certains nombres très particuliers — les coefficients binomiaux centraux — sont un phénomène rarissime (fini) ou peuvent se produire à l’infini quand on explore tous les entiers.

Ce problème fait partie des milliers de questions ouvertes laissées par Paul Erdös, connu pour avoir formulé des conjectures simples à énoncer, mais souvent redoutables à démontrer. D’abord, les coefficients binomiaux disposent d’une structure arithmétique compliquée.

Puis, les outils habituels — analyse asymptotique, théorie des nombres, calcul informatique — décrivent ce qui se passe « en général », ou localement, sans parvenir à contrôler simultanément l’ensemble des facteurs nécessaires à une coïncidence exacte. Or le problème ne porte que sur ces cas exceptionnels, et exige une preuve générale, valable pour tous les entiers, pas une accumulation d’exemples. C’est précisément ce verrou qui a résisté pendant plus de quarante ans.

Comment le problème de maths a-t-il été résolu grâce à GPT 5.2 Pro ?

Ce n’est naturellement pas la première fois que quelqu’un s’intéresse à ce problème : des mathématiciens humains en avaient déjà trouvé au moins une solution. Pour autant, cette preuve « classique » n’était ni largement diffusée, ni formalisée de manière rigoureuse ou vérifiable par ordinateur, si bien que le problème restait officiellement listé comme ouvert sur erdosproblems.com.

La résolution par IA s’est déroulée de la manière suivante : Neel Somani a fourni à GPT-5.2 Pro l’énoncé du problème et lui a demandé d’en proposer d’abord une stratégie, puis une preuve détaillée. Le modèle explore rapidement de nombreuses pistes, avant de produire une démonstration structurée — lemmes, découpage en cas, enchaînement d’arguments — parfois au prix de constructions ou de réécritures peu évidentes. La preuve est ensuite itérée : l’humain et le modèle corrigent, précisent et exigent des justifications supplémentaires. On aboutit ainsi à une version « propre » en langage mathématique (souvent en LaTeX), encore informelle, mais suffisamment détaillée pour être examinée et validée.

Pour le problème #397, GPT-5.2 Pro a produit une famille de contre-exemples qui réfutent la conjecture : il montre qu’il existe des choix d’indices donnant une égalité de produits que l’énoncé prétendait exclure. La résolution prend donc la forme d’une démonstration par contre-exemple, transformée en argument rigoureux.

Ensuite, la preuve obtenue est soumise à Aristotle, un système d’IA développé par la start-up Harmonic, chargé de la formaliser. Pour cela, Aristotle s’appuie sur Lean, un langage de programmation servant d’assistant de preuve mathématique, dans lequel les énoncés et les démonstrations sont écrits sous forme de code.

Concrètement, Aristotle commence par traduire l’énoncé informel en un théorème précis dans Lean, puis découpe la démonstration en lemmes élémentaires (de petits résultats intermédiaires). Chaque étape est ensuite réécrite dans le langage formel de Lean, en utilisant la bibliothèque mathématique de référence, mathlib. Le noyau logique de Lean vérifie alors mécaniquement que chaque transition est correcte, sans aucune place pour l’ambiguïté. Lean joue ainsi le rôle d’arbitre : soit la preuve est acceptée dans son intégralité, soit elle est rejetée. Dans le cas présent, la preuve ainsi formalisée a ensuite été relue et approuvée par Terence Tao, l’un des mathématiciens les plus respectés au monde.

Il n’y a pas que la résolution qui frappe : GPT-5.2 Pro et Aristotle auraient enchaîné plusieurs problèmes d’Erdös en quelques jours (bien que ces derniers ne soient pas détaillés), là où de tels problèmes peuvent demander des mois, voire des années de travail humain. Si démêler un problème de Paul Erdös ne constitue pas un séisme mathématique absolu, la méthode employée, elle, change la donne.

Pour la première fois, une combinaison de modèle généraliste, d’assistant de preuve formel et d’experts humains montre qu’il est possible de confier à une IA non seulement des calculs ou des conjectures, mais des démonstrations complètes, contrôlées ligne à ligne par un noyau logique. Reste désormais à savoir jusqu’où les mathématiciens accepteront de partager ce travail de preuve avec leurs nouvelles co-auteures algorithmiques.

Toute l'actu tech en un clin d'œil

Ajoutez Numerama à votre écran d'accueil et restez connectés au futur !

Installer Numerama