Maths : l'IA d'OpenAI a résolu 372 problèmes, et personne ne comprend ses preuves

Mardi 6 octobre, six heures du soir à New York. OpenAI dépose sur GitHub, le grand entrepôt où les développeurs partagent leur code, un dossier de 719 articles de mathématiques. Pas des exercices de lycée : 372 résultats sur des problèmes que des chercheurs n'arrivaient pas à résoudre depuis des années, parfois des décennies. Tous écrits par une IA maison qu'OpenAI n'a même pas encore nommée. Le lendemain, Scott Aaronson, un des chercheurs en informatique les plus connus des États-Unis, écrit sur son blog que c'est « sûrement l'un des plus grands jours de l'histoire des mathématiques ». Rien que ça !

Et le pire, c'est qu'il ajoute qu'à peu près aucun humain n'a encore compris ces preuves.

Livraison de 719 articles. Signature ici, et bon courage pour la relecture

La conjecture d'une vie, réglée en une nuit

Une conjecture, c'est une affirmation que tout le monde croit vraie, mais que personne n'a réussi à démontrer. Tant qu'il n'y a pas de preuve, ça reste un pari, même si toute la profession parie dans le même sens.

Dans le lot d'OpenAI, il y a une preuve de la « conjecture des jeux uniques », posée en 2002 par le chercheur Subhash Khot. En gros, elle dit que pour toute une famille de problèmes, même trouver une réponse à peu près correcte est aussi dur que trouver la réponse parfaite. Ça a l'air abstrait, mais c'est une des grandes questions de l'informatique théorique depuis vingt-quatre ans. Et la femme d'Aaronson, Dana Moshkovitz, elle aussi chercheuse, a travaillé dessus pendant toute sa carrière.

Sa réaction, rapportée par son mari : la preuve est « si horriblement écrite qu'il est impossible de la lire sans l'aide d'une IA », et elle donne l'impression d'avoir été écrite « par quelqu'un sous psychédéliques ». Imagine passer vingt ans de ta vie sur une question, y penser sous la douche, en vacances, pendant les repas de famille, et recevoir la réponse un mardi soir, en vrac, dans un charabia que tu dois faire traduire par une autre machine pour comprendre ce qu'on t'a pris. Aïe.

Comment on vérifie une preuve que personne ne sait lire ?

Une partie des preuves est livrée avec une vérification écrite en Lean, un logiciel qui relit un raisonnement mathématique étape par étape et refuse d'avancer s'il y a le moindre trou. Un peu comme un correcteur d'orthographe, mais pour la logique : il ne comprend pas l'idée, il vérifie juste que chaque marche de l'escalier est bien posée sur la précédente.

Mais d'après le site spécialisé Implicator, au 7 octobre, seuls 300 manuscrits sur 719 avaient leur vérification Lean. À peine plus de quatre sur dix. Et il y a un piège que les mathématiciens ont tout de suite pointé : Lean vérifie que la preuve est juste pour l'énoncé tel qu'il a été tapé dans la machine. Si quelqu'un a mal recopié l'énoncé, la preuve peut être parfaite et répondre à une autre question que celle qu'on se posait. Bref, un tampon « vérifié » sur une copie que personne n'a lue.

Vérifié. Compris, c'est une autre affaire

Et ça n'a pas traîné : dès le 7 octobre, OpenAI a retiré trois manuscrits à cause d'une erreur de signe, un plus qui aurait dû être un moins, et en a corrigé quatorze autres. C'est exactement le genre de chose qu'une vraie relecture attrape, et c'est rassurant de voir que quelqu'un relit. Moi qui relis tous les jours du code écrit par Claude Code, je connais très bien cette sensation : un truc qui marche, et tu ne sais pas encore pourquoi.

372 problèmes résolus, mais sur combien ?

Le chiffre de 372 impressionne, mais il faut le remettre à sa place. D'après Aaronson, l'IA a été lancée sur environ 8 000 problèmes, avec à peu près trois heures de calcul chacun, et elle en a résolu autour de 5 %. Quatre-vingt-quinze pour cent d'échecs, donc. Ça reste énorme, parce que ces 5 % sont des problèmes que des humains n'avaient pas résolus, mais ce n'est pas une machine qui règle tout ce qu'on lui donne. Et aucun de ces résultats ne règle les plus grandes questions du domaine. C'est le chercheur Lance Fortnow qui le rappelle. Lui, pourtant, a retrouvé dans la liste une question qu'il avait posée dans sa propre thèse, en 1989. Trente-sept ans d'attente !

Andrew Sutherland, mathématicien au MIT, le dit sans détour : tant qu'OpenAI ne publie pas son modèle et que personne ne peut refaire l'expérience, il faut traiter ces annonces comme non vérifiées. Et il a raison sur un point précis : OpenAI n'a publié ni ses consignes, ni son modèle, alors qu'un groupe de mathématiciens qui la conseille les avait demandés fin septembre. Pendant ce temps, une association de mathématiciens appelle carrément à boycotter OpenAI, en parlant d'une « démonstration de force ».

Aaronson, lui, a trouvé la comparaison qui fait mal : les mathématiciens sont comme un chasseur-cueilleur qui a passé sa vie à apprendre à survivre dans une forêt hostile, et qui voit un matin un immense hôtel de luxe pousser juste à côté de sa cabane, avec héliport et piscines chauffées.

Trente ans à apprendre à faire du feu avec deux bâtons. Et l'hôtel d'en face a le chauffage au sol

Et toi, ça te sert à quoi ?

Demain matin ? À rien du tout. Mais regarde un des résultats de la liste : une façon plus rapide de multiplier entre eux deux grands tableaux de nombres, ce que les matheux appellent des matrices. C'est l'opération que la carte graphique de ton PC répète des milliards de fois par seconde pour faire tourner un jeu, un filtre photo ou une IA. L'IA a donc trouvé comment faire plus vite son propre calcul. Elle se bricole le moteur !

Par contre, calmons-nous. Depuis les années 1990, les records de ce genre sont presque tous restés sur le papier : ils ne deviennent plus rapides que pour des tableaux tellement gigantesques qu'aucun ordinateur au monde ne les manipulera jamais. Rien ne dit que celui-là fera exception. Ça peut prendre dix ans, vingt ans, ou ne jamais sortir des revues.

Le vrai changement pour toi est ailleurs, et il est plus lent : les maths, c'est la fondation sur laquelle tout le reste est construit, des prévisions météo au calcul de la résistance d'un pont, en passant par le petit cadenas de ton navigateur qui protège ta carte bancaire. Si une machine fait avancer cette fondation plus vite que des générations de chercheurs, tout ce qui est bâti dessus finira par en profiter. Mais pas cette année.

On a d'ailleurs déjà vécu ça. En 1976, deux chercheurs démontrent avec l'aide d'un ordinateur qu'il suffit de quatre couleurs pour colorier n'importe quelle carte sans que deux pays voisins aient la même couleur. Plus de mille heures de calcul, impossible à vérifier à la main. Les mathématiciens ont grogné pendant des années, certains refusaient d'appeler ça une preuve. En 2005, elle a été entièrement revérifiée par un logiciel du même genre que Lean, et plus personne ne la conteste aujourd'hui.

1976 : quatre couleurs, mille heures de calcul, et vingt ans de mauvaise humeur

Il y a quatre jours, je me demandais si l'IA de Meta avait vraiment résolu cinq problèmes inédits. Cinq ! Le lendemain, OpenAI en annonçait 372.

Mon avis

Je trouve ça fascinant, et en même temps je comprends parfaitement la colère des mathématiciens. Fascinant parce que des questions qui résistaient depuis vingt ans viennent de tomber, et qu'on va apprendre des choses en les décortiquant. Mais livrer 719 articles d'un coup, illisibles, sans le modèle ni les consignes, et laisser les chercheurs du monde entier se débrouiller pour faire le tri, ce n'est pas comme ça qu'on fait de la science. On pose les cartons devant la porte, et on s'en va !

Alors aux étudiants en maths qui se demandent ce matin s'ils ont choisi le bon métier : vous l'avez choisi ! Quelqu'un va devoir lire tout ça, et ce n'est pas la machine qui va le faire !

Sources

• OpenAI, 6 octobre 2026 : annonce de la publication des résultats mathématiques
• OpenAI sur GitHub : le dossier des 719 manuscrits
• Scott Aaronson, 7 octobre 2026 : « The Mathocalypse » (8 000 problèmes, 5 %, réaction de Dana Moshkovitz)
• Lance Fortnow, 7 octobre 2026 : « Open No More »
• Implicator : vérification Lean, manuscrits retirés, réaction d'Andrew Sutherland
• The Decoder : des mathématiciens appellent au boycott d'OpenAI

Article écrit avec l'aide de Claude Code, relu et corrigé par moi.