L’IA vient-elle de résoudre un grand problème de maths ? OpenAI déverse 719 preuves d’un coup

Mardi 6 octobre, 18 heures, heure de New York. Sans tambour ni trompette, OpenAI dépose sur GitHub un dossier baptisé tout sobrement « math ». À l’intérieur : 719 manuscrits de démonstrations mathématiques, regroupés en 372 « familles » de problèmes, tous produits par un modèle d’IA interne que personne, hors de l’entreprise, n’a jamais utilisé.

Le lendemain, l’informaticien Scott Aaronson titre son billet de blog « The Mathocalypse » et parle de « l’un des plus grands jours de l’histoire des mathématiques ». Au même moment, d’autres chercheurs grincent des dents et dénoncent des « maths en vrac » impossibles à relire. Qui croire ? On remet de l’ordre dans ce tohu-bohu, sans équation, promis.

🔵 Pour les débutants : c’est quoi une « conjecture » ? Une conjecture, c’est une affirmation que les mathématiciens soupçonnent vraie (ou fausse), mais que personne n’a encore réussi à démontrer. Certaines résistent depuis des siècles. Tant qu’il n’y a pas de preuve, ce n’est qu’une intuition, aussi solide soit-elle. Une démonstration (ou preuve), c’est l’enchaînement de raisonnements logiques qui établit, une fois pour toutes, qu’un énoncé est vrai.

Ce qu’OpenAI a vraiment publié

• 719 manuscrits selon le dépôt GitHub (722 selon Scientific American, la petite différence tient sans doute à des mises à jour du dépôt).
• 372 familles de résultats, c’est-à-dire autant de problèmes ou de pistes ouvertes attaquées.
• Environ 4 000 problèmes ont été soumis au modèle. Seuls ceux jugés suffisamment significatifs ont été retenus.
• Environ 42 % des résultats principaux ont été formalisés dans Lean, un logiciel qui vérifie mécaniquement chaque étape d’une preuve.
• En moyenne, chaque résultat a consommé l’équivalent de trois heures de « réflexion » de ChatGPT Pro.
• Selon OpenAI, la quasi-totalité est sortie d’un seul prompt confié à un seul agent IA, même si certains problèmes ont nécessité plusieurs tentatives.

Ce dernier point est loin d’être anodin. En septembre, pour sa démonstration très médiatisée autour des équations de Navier-Stokes (on vous la racontait ici même), OpenAI avait lancé un essaim de 10 000 agents pour une facture de calcul estimée à plusieurs millions de dollars. Cette fois, la méthode est présentée comme presque artisanale : une consigne, un agent, quelques heures.

Les résultats qui font tourner les têtes

Parmi les centaines de manuscrits, quelques titres ont immédiatement fait réagir la communauté :

Problème	De quoi s’agit-il, en clair ?	Statut annoncé
Conjecture de Kakeya en dimension 4	Quelle place minimale faut-il pour faire pivoter une aiguille dans toutes les directions ? Résolue en 3D en 2025, restait ouverte en 4D.	Solution revendiquée
Hypothèse de Riemann	Le plus célèbre problème ouvert des maths, lié à la répartition des nombres premiers. 1 million de dollars à la clé.	Avancée partielle, PAS une résolution
Conjecture des jeux uniques (UGC)	Une question d’informatique théorique : certains problèmes sont-ils impossibles à résoudre même approximativement ?	Preuve « probable » selon S. Aaronson
Exposant d’irrationalité de π	À quel point π peut-il être approché par des fractions ?	Résultat mis en avant par OpenAI
Conjecture de Hodge (cas particulier)	Un des 7 problèmes du millénaire, ici dans un cas très restreint (variétés abéliennes CM).	Cas particulier revendiqué

Kakeya, ou l’aiguille qui tourne

Prenez une aiguille posée sur une table. Vous voulez la faire pivoter pour qu’elle pointe successivement dans toutes les directions. Quelle est la plus petite surface nécessaire ? Intuitivement, on pense à un disque. Or, le mathématicien Abram Besicovitch a montré dès les années 1920 qu’on peut ruser avec des figures biscornues dont la surface est aussi petite qu’on veut. La conjecture de Kakeya, elle, affirme que ces ensembles, même minuscules, restent « gros » d’une autre manière (leur dimension reste maximale). Résolu en 3 dimensions en 2025 par des humains, le cas 4D était toujours ouvert. Si la preuve de l’IA tient, c’est une vraie pépite.

Riemann : on se calme

Plusieurs titres racoleurs ont parlé d’une IA qui « s’attaque à Riemann ». Nuance capitale : OpenAI revendique une avancée (une zone où la fonction zêta n’a pas de zéros), pas une démonstration de l’hypothèse. Le chèque d’un million de dollars du Clay Institute reste au coffre. Et le dépôt précise lui-même que ce manuscrit a été retouché par des humains pour être lisible.

🔴 Attention : un résultat publié n’est pas un résultat validé Lean garantit que la logique d’une preuve formalisée est correcte, mais moins de la moitié des résultats principaux sont formalisés. Pour le reste, OpenAI écrit noir sur blanc que « certains résultats non formalisés pourraient comporter des problèmes ». Et même une preuve vérifiée par Lean peut démontrer… autre chose que ce qu’on croit, si l’énoncé a été mal traduit au départ.

Lean, le correcteur qui ne dort jamais

Imaginez un professeur de maths d’une rigueur maladive, qui refuse la moindre étape « évidente » et exige que tout soit justifié jusqu’aux axiomes. C’est Lean. On y traduit une preuve dans un langage informatique très strict, et le logiciel vérifie, ligne après ligne, qu’aucune faille ne s’est glissée.

C’est précisément ce qui rend la période fascinante : pour la première fois, une machine produit des preuves et une autre machine les contrôle. L’humain, lui, se retrouve à la toute fin de la chaîne, chargé de juger si le résultat est intéressant… et de le comprendre.

Pourquoi les mathématiciens sont divisés

Le camp de l’enthousiasme

• Scott Aaronson (Université du Texas) parle d’un changement de paradigme et appelle à ne pas balayer ces résultats d’un revers de main.
• Sa compagne, la théoricienne Dana Moshkovitz, spécialiste du sujet, estime que la conjecture des jeux uniques est vraie, et que la preuve proposée construit un nouveau type de code arborescent. Elle ajoute toutefois, avec un humour féroce, que le texte est « si horriblement écrit qu’il est impossible de le lire sans l’aide d’une IA ».

Le camp de la méfiance

• Andrew Sutherland (MIT) : tant qu’OpenAI ne publie pas le modèle et que d’autres ne peuvent pas reproduire les résultats, l’histoire du « prompt unique » reste invérifiable.
• Un groupe consultatif de l’Institute for Advanced Study de Princeton avait recommandé de publier le nom du modèle, les prompts exacts et le temps de calcul par problème. OpenAI n’a donné que des moyennes et a gardé ses prompts.
• En septembre, 25 lauréats de la médaille Fields (le « Nobel des maths ») ont signé une déclaration intitulée « Un grave désalignement de l’IA en mathématiques ». Leur argument : résoudre des problèmes n’est qu’un moyen, le vrai but des maths est la compréhension. Produire des énoncés à la chaîne pourrait abîmer les fondations de la discipline.
• Une lettre ouverte de mathématiciens de Caltech, signée par 771 personnes, a même popularisé l’expression « slop mathematics » : des résultats balancés vite, que d’autres devront vérifier gratuitement.

🟡 Imaginez qu’un inconnu dépose 719 romans policiers à la bibliothèque en affirmant que chacun résout une vraie affaire non élucidée. Certains sont visiblement brillants. D’autres mal écrits. Personne n’a le temps de tout lire, et l’auteur refuse de dire comment il a enquêté. Excitant ? Oui. Rassurant ? Pas complètement.

Alors, l’IA a-t-elle résolu un grand problème ?

La réponse honnête tient en trois temps :

• Probablement oui, pour certains problèmes ouverts réels, surtout ceux vérifiés dans Lean. Ce ne sont pas des exercices de lycée : ce sont des questions sur lesquelles des chercheurs ont buté pendant des années.
• Non, pour les monstres sacrés. Ni l’hypothèse de Riemann, ni la conjecture de Hodge dans sa forme générale ne sont résolues.
• Il faudra des mois, voire des années, pour que la communauté digère ce volume et distingue les idées vraiment neuves des simples recombinaisons de techniques connues.

Ce qui change, en revanche, c’est l’échelle. Un mathématicien humain publie quelques articles par an. Une IA vient d’en déposer des centaines en une soirée. Le goulot d’étranglement n’est plus la découverte : c’est la relecture. Et ça, personne n’y était préparé.

Et pour vous, concrètement ?

Vous n’allez pas démontrer de théorèmes ce week-end, d’accord. Mais les conséquences peuvent ruisseler jusqu’à votre quotidien :

• Des algorithmes plus rapides : plusieurs résultats portent sur l’informatique théorique. Un calcul plus efficace, c’est à terme des logiciels plus économes.
• Une IA plus fiable : un modèle capable de raisonner sans se tromper sur des preuves longues est un modèle qui hallucine moins sur vos tâches à vous.
• Un nouvel usage étudiant : demander à une IA de vérifier une démonstration, étape par étape, devient un vrai exercice d’apprentissage.

On assiste à quelque chose d’historique, mais d’historique en brouillon. Le vrai test, ce n’est pas le nombre de preuves déposées, c’est le nombre qui survivra à la relecture, et surtout le nombre qui nous aura appris quelque chose de neuf.

• Une preuve que personne ne comprend, mais qu’une machine certifie juste, est-ce encore des mathématiques ?
• OpenAI devrait-il être obligé de publier ses prompts et son modèle pour que ses résultats soient pris au sérieux ?
• Les médaillés Fields ont-ils raison de craindre une « industrialisation » des maths, ou est-ce un réflexe corporatiste ?

Source : GitHub : dépôt openai/math