Analyse technique 019｜openai/math : Analyse du dépôt où OpenAI rend open source 722 manuscrits mathématiques d'IA en une seule fois

Le 6 octobre, OpenAI a rendu public le dépôt openai/math sur GitHub, publiant en une seule fois les résultats de recherche mathématique produits par un modèle interne non publié : 722 manuscrits, 372 familles de résultats, 3.1 GB, 132,880 fichiers, 9,832 étoiles en deux jours (toujours en hausse), la discussion associée sur HN (Hacker News) dépassant les 1,200 votes positifs et 1,400 commentaires, le blog officiel « Sharing AI progress in mathematics » étant publié le même jour. Ce n’est pas une collection d’articles, mais un trio « manuscrit + formalisation + outil de vérification », et la façon de le lire, de le vérifier et les controverses autour de ce dépôt reposent presque entièrement sur cette structure en trois couches. Cet article l’analyse selon six aspects : ce que c’est, pourquoi cela vaut la peine d’être regardé, la structure et le mécanisme, les chiffres et les limites, comment le vérifier, et le jugement de valeur.

I. Qu’est-ce que c’est

openai/math est un dépôt de production mathématique par IA : langage principal Lean, licence Apache-2.0, trois couches de contenu plus une carte des manuscrits.

Première couche preprints/, 722 répertoires, un répertoire par manuscrit de recherche, contenant paper.pdf, les fichiers sources LaTeX, les citations et les instructions de construction. Les noms des répertoires comportent une date : au plus tôt le 10 septembre — jour même de l’annonce publique des résultats de Navier-Stokes — au plus tard le 5 octobre, la publication ayant eu lieu le 6 octobre. Les manuscrits ont été accumulés pendant près d’un mois avant d’être publiés d’un coup, l’horodatage du premier commit correspondant au jour même de la publication.

Deuxième couche lean/, bibliothèque de formalisation. Sous OAI/, 24 sous-répertoires par discipline, de Algebra à Topology, avec 121 700 fichiers .lean ; elle dépend de mathlib47 et est verrouillée sur le commit spécifique d13f23b, patches/ contient les correctifs pour l’amont — cette bibliothèque ne fait pas que consommer mathlib4, elle a modifié l’amont.

Troisième couche reasoning_traces/, des PDF résumant le raisonnement pour 10 familles de résultats. Le README les qualifie d’abridged summaries, mais des commentaires sur HN (Hacker News) font remarquer qu’une description plus exacte serait « des extraits de résumés » — et non les traces de raisonnement originales.

Navigation de premier niveau en deux fichiers : CONTENTS.md, une carte des manuscrits de 640 Ko, répertoriant les 722 manuscrits un par un, en indiquant pour chacun le titre et la référence à la conclusion ; les numéros 001, 003, 102 et 180 cités ci-dessous correspondent aux entrées de cette carte. overview.pdf, accompagné de ses fichiers sources, fait 323 Ko et sert de guide pour l’ensemble des résultats. Le dépôt est organisé en « familles » : un résultat principal accompagné d’arguments associés, de corollaires et de preuves alternatives forme une famille ; les 722 manuscrits sont répartis dans 372 familles — une part non négligeable des résultats est publiée avec ses preuves alternatives ou ses arguments associés, il est donc plus efficace de lire par famille que par article.

II. Pourquoi il vaut la peine de s’y intéresser maintenant

La première raison est le poids de la liste de résultats elle-même. Les 722 documents ne sont pas 722 problèmes isolés, organisés par familles, ils ressemblent davantage à un dossier de recherche ; dans CONTENTS.md, outre les entrées majeures, sont également dispersés l’exposant d’irrationalité de π, la borne quasi-polynomiale des progressions arithmétiques de type Erdős, le contre-exemple de Kaplansky sur la finitude directe en caractéristique 2, l’isomorphisme des facteurs de groupes libres, l’équation de Vlasov–Maxwell relativiste, la conjecture de Mahler, l’aimantation spontanée du ferromagnétique de Heisenberg quantique — s’étendant de la théorie des nombres et de la théorie des graphes jusqu’à la physique mathématique. Sélectionnons quatre des entrées majeures pour en parler.

Le numéro 003, la quasi-hypothèse de Riemann : la fonction ζ et toutes les fonctions L de Dirichlet n’ont pas de zéro dans la région Re(s)>7/8, avec l’exclusion uniforme des zéros de Landau–Siegel. La direction doit d’abord être clarifiée : plus la région sans zéro est à droite, plus elle est forte, le record humain est 11/12≈0.9167, 7/8=0.875 est à sa gauche — il s’agit de la borne inférieure que ce système a fait avancer de manière indépendante sur un vieux problème, et non d’un record battu.

Le numéro 102, la conjecture Unique Games (Khot, 2002), le manuscrit donne une preuve de sa validité. Une proposition de niveau infrastructure en informatique théorique, un grand nombre de résultats d’inapproximabilité la prennent comme prémisse, des commentaires sur HN (Hacker News) estiment que son poids est plus lourd que certains problèmes du millénaire.

Le numéro 180, la conjecture de Barnette (1969) : chaque graphe fini simple cubique biparti planaire 3-connexe possède un cycle hamiltonien. Un problème ouvert de 57 ans en théorie des graphes, un utilisateur de HN a raconté avoir attaqué ce problème avec les modèles les plus puissants du moment pendant des mois sans résultat.

Le numéro 001, la conjecture de rationalité de Milne (variétés abéliennes), dans la même entrée figure également la proclamation de preuve du cas spécial de la conjecture de Hodge pour les variétés abéliennes CM — il faut être précis : il s’agit seulement de la proclamation d’un cas spécial, l’authentification par l’Institut Clay n’a pas eu lieu.

La deuxième raison est la forme de la publication. Auparavant, les annonces publiques en mathématiques IA étaient pour la plupart des déclarations ponctuelles, publier d’un seul coup 722 documents, avec un dépôt complet incluant sa propre couche de formalisation et ses outils de vérification, cette forme est en soi rare. Dans les discussions sur HN, de nouvelles façons de faire sont déjà apparues : certains ont fourni le dépôt entier à leur propre agent, lui demandant de répondre point par point à la significance de chaque manuscrit — l’échelle de 722 documents a forcé l’émergence de nouveaux modes de lecture.

III. Mécanismes techniques fondamentaux

Le pipeline de production est décrit dans le README : la grande majorité des résultats sont produits par le même modèle interne non publié selon un processus fixe ; environ 4000 problèmes ont été alimentés au total, consommant en moyenne une puissance de réflexion équivalente à 3 heures de ChatGPT Pro par résultat ; les productions sont agrégées en familles, et 722 exemplaires sont conservés après avoir franchi le seuil de significativité. Deux éléments sont listés comme exceptions au processus fixe : la région sans zéro de la fonction zêta de Riemann et le cas de Hodge des variétés abéliennes CM. Le README ne détaille pas les différences, indiquant seulement que l’article sur la région sans zéro a été édité et peaufiné manuellement pour la lisibilité.

L’organisation de la couche de formalisation mérite d’être examinée en détail. Sous lean/docs/, chaque résultat formalisé dispose d’une page de document, indiquant clairement le domaine d’application, l’article de référence et le lien Comparator. Prenons encore le numéro 003 comme exemple : l’énoncé couvre la fonction ζ, toutes les fonctions L de Dirichlet et les fonctions L de Hecke d’ordre fini sur Q(√-3) ; le pôle du caractère principal en s=1 est explicitement exclu de l’énoncé ; les constantes ne sont pas données de valeur explicite. Ce qui est formalisé et ce qui ne l’est pas est clairement délimité dans la documentation — pour lire ce dépôt, lisez d’abord les docs puis le code, et ces pages d’explication constituent le point d’entrée le plus facile.

Il faut cependant tempérer les attentes concernant la couche des résumés de raisonnement. 10 familles sont dotées de reasoning_traces, le README les qualifie d’abridged summaries, et les discussions sur HN (Hacker News) soulignent qu’il s’agit en fait d’« extraits de résumés ». Comparé au volume de réflexion de « 3 heures en moyenne par résultat », les matériaux de raisonnement mis à la disposition de la communauté sont loin d’être suffisants pour reproduire le chemin de raisonnement du modèle — pour ceux qui souhaitent étudier « comment le modèle pense », c’est la couche la plus opaque du dépôt.

La stratification de la vérification est le maillon le plus crucial du mécanisme. formalization.yaml dénombre 162 articles dont le résultat principal est formalisé, représentant un peu plus de 20 % des 722 ; le README indique textuellement que les résultats se trouvent à différentes étapes de vérification, que tous ne sont pas accompagnés d’une formalisation Lean, et reconnaît que les parties non formalisées peuvent contenir des erreurs. Autrement dit, le dépôt lui-même étiquette la crédibilité sous forme de gradient : 162 articles sont vérifiables par machine, tandis que les 560 autres sont des affirmations lisibles par l’homme.

4. Nombres et limites

Récapitulatif des chiffres : 722 manuscrits, 372 familles, 162 formalisations, 132,880 fichiers, 3.1 GB, environ 4000 problèmes alimentés, 3 heures en moyenne par résultat, 9832 étoiles en deux jours ; bibliothèque Lean (logiciel de preuve) : 24 sous-répertoires disciplinaires, 121 700 fichiers .lean.

Quatre limites sont à souligner.

Premièrement, il ne faut pas interpréter la direction à l’envers. 7/8 est inférieur à 11/12, le résultat de l’IA sur la région sans zéro ne constitue pas un dépassement de l’humain ; l’écrire comme un record battu est l’erreur la plus courante sur ce sujet, et se tromper de sens ruine la crédibilité de l’ensemble de l’article.

Deuxièmement, la formalisation n’exclut pas les erreurs. La prémisse de la vérification par Lean est que l’énoncé du théorème a été correctement traduit — la machine vérifie l’énoncé figurant dans le code, et non la conclusion en chinois ou en anglais de l’article. Les critiques très votées sur HN (Hacker News) portent précisément sur ce point : couvrant 24 disciplines, la traduction de chaque énoncé mérite un examen humain, et le fait que le document 003 ne donne pas de valeur explicite pour les constantes est le type de détail que ce genre de vérification doit scruter ; certains prédisent directement un échec, tandis que les répondants soulignent que le README (fichier lisez-moi) admet déjà que les parties non formalisées peuvent contenir des erreurs.

Troisièmement, la publication ne vaut pas certification. Le titre du blog utilise sharing et non solving, la certification Clay (Institut de mathématiques) et l’évaluation par les pairs ne se sont pas produites, l’article est signé OpenAI (entreprise d’IA), sans signature de réviseur humain. Le débat sur HN entre GitHub (plateforme de code) et arXiv (archive de prépublications) est également né de cela : certains louent la publication sur GitHub pour briser le paywall, des mathématiciens rétorquent que les résultats mathématiques passent de toute façon par arXiv, et que la valeur d’archivage du dépôt n’est pas isomorphe à celle de l’archivage d’un article.

Quatrièmement, la mesure de la puissance de calcul exige de regarder en coulisses, et la mesure du nombre d’étoiles dépend de l’objet visé. 3 heures est une mesure de moyenne, quelqu’un sur HN a ressorti les antécédents de AlphaZero (programme d’IA) — le « super-humain en 4 heures » était en réalité 4 heures multiplié par 5000 blocs TPU (processeurs) — rappelant que des expressions comme « 3 heures équivalent ChatGPT Pro (abonnement IA) » nécessitent de s’interroger sur la quantité totale en coulisses ; alors que 9832 étoiles en deux jours mesurent le niveau d’attention, et non l’exactitude — le dépôt lui-même a marqué les 722 copies comme gradient de vérification, et la révision communautaire ne fait que commencer.

5. Comment l’exécuter, qui peut s’y essayer

Il est possible de vérifier sans exécuter le modèle, c’est la partie la plus concrète de la conception du dépôt. lean/README donne le processus de Comparator (comparateur) : installez d’abord les trois éléments comparator, landrun et lean4export, lake update tire les dépendances, lake exe cache get récupère le cache de mathlib4, puis exécutez lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json — pour exécuter une vérification comparative sur l’énoncé formalisé numéro 003. ComparatorChallenges/ contient la liste des défis prédéfinis officiellement ; en suivant ce processus, on peut vérifier chaque élément par échantillonnage. Pour compiler l’intégralité de la bibliothèque, le README avertit spécifiquement que la limite par défaut de vm.max_map_count sous Linux (système d’exploitation) pourrait être insuffisante, et donne une solution de contournement avec CMake -DMMAP=OFF et GLIBC_TUNABLES — le fait qu’un dépôt soit si volumineux que l’officiel doive rédiger des instructions spéciales pour éviter les pièges de compilation est précisément une preuve de son ampleur.

Cela s’adresse à trois catégories de personnes. Ceux qui travaillent sur Lean (langage de preuve) et les mathématiques formalisées : les 162 résultats formalisés accompagnés d’articles et de documents de référence, ainsi que le verrouillage et les correctifs de mathlib4, constituent des actifs qui peuvent être lus et vérifiés directement, et sont également des échantillons prêts à l’emploi pour observer « comment les productions de l’IA (intelligence artificielle) atterrissent dans Lean ». Ceux qui travaillent en informatique théorique : le manuscrit sur les Unique Games (jeux uniques), qu’il soit finalement valide ou non, mérite d’être lu ligne par ligne — les implications sur le paysage de l’inapproximabilité sont trop vastes, et chaque étape de la vérification des conclusions sera citée à maintes reprises par la communauté académique. Ceux qui travaillent sur l’évaluation des modèles : l’ensemble du pipeline de filtrage comprenant l’alimentation en 4000 problèmes, l’agrégation en familles et le seuil de significativité, ainsi que le barème de coût de 3 heures par résultat, constituent une ressource méthodologique de première main rare et précieuse.

Pour ceux qui veulent juste observer, le seuil d’entrée est l’espace disque et la patience : un clone de 3.1 GB, plus une compilation de l’intégralité de la bibliothèque qui n’est pas forcément facile à digérer ; pour ceux qui ne veulent rien installer, commencez par lire le fichier overview.pdf de 323 KB à la racine ; en vingt minutes, vous aurez une vue d’ensemble des résultats du dépôt, puis vous pourrez décider dans quel répertoire disciplinaire vous diriger.

VI. Jugement de valeur et à qui cela convient

L’échantillon a une grande valeur. Il transforme « l’IA qui fait des mathématiques » d’une simple affirmation dans un communiqué de presse en un dépôt public dénombrable, vérifiable par sondage et re-vérifiable par machine. Le chiffre 162 est particulièrement crucial : même si tout le reste est sujet à caution, les énoncés formalisés de ces 162 articles constituent du contenu tangible que la communauté peut vérifier indépendamment. La déclaration du lauréat de la médaille Fields Terence Tao sur Mastodon (citée par HN) va dans le même sens : il espère que l’IA puisse expliquer ses résultats aux mathématiciens humains, et estime que l’IA peut apporter une contribution positive en matière d’explication et de construction de communauté.

La valeur en termes de productivité dépend des individus. Pour les chercheurs en mathématiques et en informatique théorique, c’est une réalité incontournable, ne serait-ce que pour vérifier si leur propre sujet a été devancé — sur HN, des doctorants ont déjà exprimé l’anxiété de « voir leur article à moitié écrit frappé par 722 articles », et les réponses empathiques conseillent d’embrasser l’avant-garde et de ne pas coller le texte original de recherches non publiées à l’IA. Ce sentiment constitue en soi une variable du secteur. Du côté de l’ingénierie, la chaîne d’outils de vérification et la documentation pour éviter les pièges de compilation constituent une référence clé en main pour les grands projets Lean. Pour ceux qui ne souhaitent que des conclusions, un rappel : il n’y a pas de conclusions ici, seulement des affirmations à différents stades de vérification.

Le blog promet également de financer une série d’ateliers, de conférences et de projets spéciaux pour aider la communauté mathématique à comprendre les résultats majeurs produits par l’IA, et déclare œuvrer à la diffusion responsable des modèles générant ces résultats ; le README mentionne également l’exploration de dépôts hébergés par la communauté. Pour conclure, un mot sur le contexte : les dix problèmes Lean d’août, la déclaration du lauréat de la médaille Fields de septembre et la proposition du groupe consultatif constituent le contexte externe de ce mode de publication ; le développement des critiques se trouve dans l’article sur les sujets brûlants du même jour et ne sera pas détaillé ici.

Jugement en une phrase : la place historique d’openai/math ne dépend pas du nombre d’articles qui résisteront à l’épreuve parmi les 722, mais du fait que c’est la première fois que la production de l’IA mathématique est placée sur une/une voie où les mathématiques humaines peuvent la vérifier un par un — le nombre d’étoiles appartient à OpenAI, le droit de vérifier un par un appartient à la communauté.

Sources de référence

• Dépôt principal : github.com/openai/math (après clonage local, comparaison élément par élément de README, CONTENTS.md, du répertoire lean/, de formalization.yaml, de git log ; aucune construction n’a été exécutée)
• Blog OpenAI « Sharing AI progress in mathematics » (2026-10-06)
• HN story 49984923 (à la date du 2026-10-08, plus de 1200 upvotes et plus de 1400 commentaires ; les déclarations de Terence Tao et le document de recommandation du groupe consultatif sont repris de HN, sans vérification mot à mot de l’original)
• Le nombre d’étoiles 9832★ correspond à la donnée à la date du 2026-10-08, et continue d’augmenter