GPT-5.2 Pro résout le problème d'Erdös #397 : analyse de la méthode
www.numerama.com
Résumer l'article
GPT‑5.2 Pro a résolu l’Erdös Problem #397, une énigme de combinatoire ouverte depuis 45 ans.
La solution repose sur une famille de contre‑exemples démontrant des égalités de produits de coefficients binomiaux centraux que la conjecture interdisait.
Formalisee dans Lean par Aristotle et validée par Terence Tao, la démonstration consacre un nouveau workflow IA‑humains pour la preuve mathématique.
GPT‑5.2 Pro a résolu l’Erdös Problem #397, une énigme de combinatoire ouverte depuis 45 ans.
La solution repose sur une famille de contre‑exemples démontrant des égalités de produits de coefficients binomiaux centraux que la conjecture interdisait.
Formalisee dans Lean par Aristotle et validée par Terence Tao, la démonstration consacre un nouveau workflow IA‑humains pour la preuve mathématique.
Recevez tous les soirs un résumé de l’actu importante avec Le Récap’
Le modèle d’IA GPT-5.2 Pro a résolu plusieurs problèmes de mathématiques, dont l’un, le 11 janvier 2026, était resté ouvert depuis 45 ans. Plus que le résultat, c’est la méthode — associant humains, assistant de preuve Lean et système d’IA Aristotle — qui pourrait transformer la pratique de la démonstration mathématique.
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.
Neel Somani a notamment utilisé GPT-5.2 pour résoudre le problème de maths. Source : Neel Somani / X
Neel Somani a notamment utilisé GPT-5.2 pour résoudre le problème de maths. Source : Neel Somani / X
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.
Le problème d'Erdös 397. Source : erdosproblems.com
Le problème d’Erdös 397. Source : erdosproblems.com
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.
Un extrait de la solution fournie par GPT-5.2 Source : erdosproblems.com / Neel Somani
Un extrait de la solution fournie par GPT-5.2 Source : erdosproblems.com / Neel Somani
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.
Vous avez lu 0 articles sur Numerama ce mois-ci
Tout le monde n'a pas les moyens de payer pour l'information.
C'est pourquoi nous maintenons notre journalisme ouvert à tous.
Mais si vous le pouvez,
voici trois bonnes raisons de soutenir notre travail :
1 Numerama+ contribue à offrir une expérience gratuite à tous les lecteurs de Numerama.
2 Vous profiterez d'une lecture sans publicité, de nombreuses fonctions avancées de lecture et des contenus exclusifs.
3 Aider Numerama dans sa mission : comprendre le présent pour anticiper l'avenir.
Si vous croyez en un web gratuit et à une information de qualité accessible au plus grand nombre, rejoignez Numerama+.
S'abonner à Numerama+
Pour ne rien manquer de l’actualité, suivez Numerama sur Google !
Toutes les infos sur ChatGPT
Cette IA a résolu un problème mathématique ouvert depuis 45 ans
Marre de ne rien comprendre à vos comptes rendus médicaux ? OpenAI lance ChatGPT Health… mais pas pour tout le monde
GTA 6, iPhone Fold et guerre Google/ChatGPT : nos 10 prédictions pour la tech en 2026
Les 15 actus tech qui ont marqué 2025 (avec de l’IA, de l’IA et de l’IA)
« Ce sera un travail stressant », Sam Altman recrute à prix d’or la personne capable d’anticiper les dérives de ChatGPT
Crédit photo de la une : Numerama
Signaler une erreur dans le texte
À lire
Arnaques en ligne : l’IA les rend plus sophistiquées, mais elle vous aide aussi à les déjouer Humanoid Native
sponso
L'essentiel intelligence artificielle
Atlas a été présenté au CES 2026. Source : Boston Dynamics Atlas a été présenté au CES 2026. Source : Boston Dynamics
StephaneM
Raphaël Nguyen
JérémyL
emmalefevre
_TGirardon13
Laura Fluck
Marie Dufour
timtom
ombrejaune
cbonnet.96
Maxime Rollet-Panson
kevinmc
Découvre Numerama+
Les IA de Google ont battu la plupart des humains lors d'une compétition de mathématiques - Numerama
www.numerama.com
Résumer l'article
Google a fait sensation en 2024 avec ses IA AlphaGeometry 2 et AlphaProof aux Olympiades Internationales de Mathématiques, décrochant une médaille d’argent.
AlphaGeometry 2 a impressionné par sa rapidité, résolvant le problème de géométrie en seulement 19 secondes avec une solution remarquée pour son élégance.
Google envisage d’avancer ses IA mathématiques en les connectant à Gemini pour qu’elles puissent comprendre et résoudre des problèmes formulés en langage naturel humain.
Google a fait sensation en 2024 avec ses IA AlphaGeometry 2 et AlphaProof aux Olympiades Internationales de Mathématiques, décrochant une médaille d’argent.
AlphaGeometry 2 a impressionné par sa rapidité, résolvant le problème de géométrie en seulement 19 secondes avec une solution remarquée pour son élégance.
Google envisage d’avancer ses IA mathématiques en les connectant à Gemini pour qu’elles puissent comprendre et résoudre des problèmes formulés en langage naturel humain.
Recevez tous les soirs un résumé de l’actu importante avec Le Récap’
Google a réussi à placer ses IA AlphaGeometry 2 et AlphaProof à deux doigts de la médaille d’or des Olympiades Internationales de Mathématiques. Les deux programmes ont reçu une médaille d’argent et AlphaGeometry 2 a bluffé par l’élégance et la rapidité de sa solution.
C’est un nouveau record pour une intelligence artificielle que vient de battre Google, dans un domaine très précis : les mathématiques. Ses deux programmes AlphaProof et AlphaGeometry 2 ont réussi à atteindre 28 points lors des Olympiades Internationales de Mathématiques (IMO) sur les 42 possibles, plaçant l’IA au niveau des médaillés d’argent de l’année 2024. Le seuil des 30 points aurait permis à Google d’entrer dans la catégorie des médaillés d’or.
Pour arriver à ces résultats, AlphaProof et AlphaGeometry 2 ont réussi à résoudre 4 problèmes sur les 6 présentés aux participants, dont le numéro 4, de géométrie. Les 3 autres problèmes d’algèbre et de théories des nombres sont tombés sous les raisonnements d’AlphaProof, dont le plus difficile de la compétition en théorie des nombres, résolu uniquement par 5 participants humains. Seuls les problèmes de combinatoire ont encore échappé aux calculs des intelligences artificielles de Google.
Rapidité et élégance
Pour le professeur Sir Timothy Gowers, médaillé Fields, parrain et médaillé d’or de l’IMO, que nous avons rencontré lors d’une table ronde, les produits de Google dépassent ce qu’il imaginait possible dans le domaine de l’IA : « Le fait que le programme puisse proposer une construction non évidente comme celle-ci est très impressionnant, et bien au-delà de ce que je pensais être l’état de l’art », confie-t-il.
Car dans cette compétition où de jeunes esprits sont réunis deux fois pour réfléchir pendant 4 heures et 30 minutes à 3 problèmes par jour, il est nécessaire de maîtriser tous les aspects des mathématiques pour en sortir la quintessence. Lors de la table ronde, Sir Timothy Gowers n’a cessé de répéter à quel point la solution proposée par AlphaGeometry 2 au problème 4 était non seulement juste, mais aussi élégante. Cette démonstration est le clou du spectacle, car s’il a fallu 3 jours à AlphaProof pour résoudre certains de ses problèmes, AlphaGeometry n’a pris que 19 secondes pour trouver une solution.
Impossible d’infirmer ou de confirmer les dires d’un médaillé Fields, la plus haute distinction dans le domaine des mathématiques, alors nous ferons le choix de le croire sur parole. À la fin de la conférence, Google a tout de même fourni un résumé succinct de la solution au problème proposée par AlphaGeometry, que nous reproduisons ci-dessous. La solution détaillée est disponible à cette adresse : les plus matheux de nos lecteurs pourront juger par eux-mêmes.
Illustration du Problème 4, qui demande de prouver que la somme de ∠KIL et ∠XPY est égale à 180°. AlphaGeometry 2 a proposé de construire E, un point sur la ligne BI de sorte que ∠AEB = 90°. Le point E aide à donner un but au milieu L de AB, créant de nombreuses paires de triangles similaires tels que ABE ~ YBI et ALE ~ IPC nécessaires pour prouver la conclusion.
Illustration du Problème 4, qui demande de prouver que la somme de ∠KIL et ∠XPY est égale à 180°. AlphaGeometry 2 a proposé de construire E, un point sur la ligne BI de sorte que ∠AEB = 90°. Le point E rend compte du rôle particulier du milieu L de AB en créant de nombreuses paires de triangles semblables nécessaires à la démonstration, tels que ABE ~ YBI et ALE ~ IPC. Source : Google, réutilisation autorisée pour Numerama
AlphaGeometry2 n’a pas eu un coup de chance : ce programme développé par Google est un système hybride neuro-symbolique dans lequel le modèle de langage est basé sur Gemini (oui, l’IA générative grand public dans les smartphones Pixel et sur le web) et entraîné à partir de très nombreuses données, bien plus que la version 1. Ainsi entraîné, AlphaGeometry 2 a réussi à résoudre 83 % des problèmes de géométrie des Olympiades Internationales de Mathématiques de ces 25 dernières années, quand AlphaGeometry premier du nom ne résolvait qu’un peu plus de la moitié des problèmes.
Quel avenir pour les IA mathématiciennes de Google ?
Avec un outil comme Gemini, on imagine très bien comment Google peut avancer. Aujourd’hui, AlphaGeometry 2 et AlphaProof ont besoin d’une entrée dans un langage formel pour résoudre leurs problèmes. Mais dès cette année 2024, Google a commencé à tester une association entre Gemini et ses programmes dédiés aux mathématiques.
Le but ? Tenter de faire faire à l’IA l’interface entre le langage naturel des humains (et des problèmes mathématiques) et le langage formel que les IA spécialisées comprennent. En d’autres termes, les équipes cherchent à faciliter toujours plus l’étape initiale, jusqu’à arriver à des IA qui pourraient simplement lire les problèmes, les analyser et les résoudre.
C’est déjà, à peu de chose près, la manière dont fonctionne AlphaProof, aidé de l’algorithme de renforcement AlphaZero (oui, celui-là même qui s’est auto-appris à jouer aux échecs et au jeu de Go).
Le fonctionnement d'AlphaProof avec AlphaZero
Le fonctionnement d’AlphaProof avec AlphaZero Source : Google, réutilisation autorisée pour Numerama
Mais à quoi cela sert-il de faire résoudre des problèmes de mathématiques à des ordinateurs en autonomie ? À terme, l’intérêt se situe, comme souvent, dans la recherche. Les programmes de Google pourront être des compagnons des chercheurs capables de trouver, peut-être, des solutions aux problèmes qu’ils se posent. Et comme la recherche est souvent une question de temps, en gagner grâce aux IA peut permettre aux plus brillants esprits mathématiques d’avancer encore plus vite.
Vous avez lu 0 articles sur Numerama ce mois-ci
Tout le monde n'a pas les moyens de payer pour l'information.
C'est pourquoi nous maintenons notre journalisme ouvert à tous.
Mais si vous le pouvez,
voici trois bonnes raisons de soutenir notre travail :
1 Numerama+ contribue à offrir une expérience gratuite à tous les lecteurs de Numerama.
2 Vous profiterez d'une lecture sans publicité, de nombreuses fonctions avancées de lecture et des contenus exclusifs.
3 Aider Numerama dans sa mission : comprendre le présent pour anticiper l'avenir.
Si vous croyez en un web gratuit et à une information de qualité accessible au plus grand nombre, rejoignez Numerama+.
S'abonner à Numerama+
Pour ne rien manquer de l’actualité, suivez Numerama sur Google !
À lire
L’innovation eSIM de RED by SFR : le hack technologique ultime pour vos voyages à l’international Humanoid Native
sponso
L'essentiel intelligence artificielle
Atlas a été présenté au CES 2026. Source : Boston Dynamics Atlas a été présenté au CES 2026. Source : Boston Dynamics
Laura Fluck
spaceY
ombrejaune
lealeroy
Loïc Martin
manon.andre
JérémyL
cgarcia
NaN
marine-ara
Lucas Moisel
noe-chabin
Découvre Numerama+