Le 6 octobre, OpenAI a publié 722 manuscrits de mathématiques sur GitHub, accompagnés de preuves vérifiables par ordinateur. Tous n'ont pas été validés de façon indépendante, et le modèle qui les a produits n'a même pas de nom public.
Ce qu'OpenAI a réellement mis en ligne
Le dépôt openai/math est apparu le 6 octobre, en même temps qu'une note de blog intitulée « Sharing AI progress in mathematics ». Le catalogue contient 722 manuscrits, rangés en 372 « familles » de recherche : un même ensemble regroupe un résultat principal, ses conséquences, des arguments d'accompagnement ou des preuves alternatives.
La particularité de cette publication tient au format. Chaque énoncé s'accompagne d'une formalisation en Lean, un langage de programmation qui permet de vérifier une preuve par ordinateur. Un argument mathématique ordinaire se juge à la lecture. Une preuve formalisée, elle, se juge par un vérificateur qui dit oui ou non. C'est ce qui rend le lot potentiellement plus facile à contrôler qu'un simple article.
Ces résultats proviennent, selon OpenAI, d'un modèle frontière interne resté sans nom, sans tarif public et sans API. La société indique avoir aidé à préparer les manuscrits et à formaliser les preuves, tout en précisant que la démonstration mathématique elle-même est le fait du modèle. Une répartition des rôles qu'il faut avoir en tête en lisant le dépôt.
La vérification, maillon faible du lot
La formalisation ne garantit pas que tout le contenu a été généré correctement du premier coup. Elle offre un cadre pour trancher, à condition de lancer le vérificateur, ce qui n'a pas été fait de façon systématique et indépendante. Plusieurs observateurs ont relevé que le niveau de contrôle reste inégal d'un document à l'autre. Le diable se cache là.
OpenAI reconnaît d'ailleurs des pistes d'amélioration pour les prochaines publications : meilleures citations, meilleure exposition mathématique, présentation plus claire des résultats. Une manière d'admettre que la lisibilité et la traçabilité du travail restent perfectibles.
Le contenu touche des domaines variés : mathématiques pures, informatique théorique et physique mathématique. Le site GitHub évoque environ 4 000 problèmes abordés, un volume qui dépasse largement une publication classique. Pour un domaine habitué à des articles isolés, l'échelle elle-même surprend.
Un modèle sans nom, une question ouverte
L'élément le plus déroutant est ailleurs. Le modèle qui a produit ces résultats n'est pas commercialisé. Aucun nom public, aucune page produit, aucun tarif. OpenAI le présente comme un modèle frontière interne, utilisé pour la recherche sans être exposé au grand public.
Ce choix interroge. Il sépare la capacité de recherche de la capacité vendue. Un laboratoire peut garder en coulisses un modèle plus fort que ceux qu'il propose à ses clients, en réservant ses résultats à la démonstration scientifique. Cela brouille la lecture habituelle des benchmarks, qui classent des modèles publics. Sur ce point, nous n'avons pas de moyen de comparer directement cette version interne aux modèles connus.
Il faut aussi garder en tête la spécialisation. Un modèle qui produit des preuves de haut niveau en mathématiques n'est pas forcément meilleur sur des tâches du quotidien, comme résumer un document ou tenir une conversation. La performance se mesure par domaine, pas en bloc.
Ce que cela change pour la suite
Rappelons le contexte : un débat agité traverse les mathématiques depuis plusieurs mois, à mesure que des modèles publient des résultats sans passer par la revue humaine classique. Cette publication d'OpenAI s'inscrit dans cette tendance. Mais elle déplace la question. Le point saillant n'est plus « à quelle vitesse », mais « comment vérifie-t-on ».
Pour le lecteur curieux, l'affaire a un intérêt concret. Elle montre ce qui se passe quand l'IA produit à haute fréquence un savoir qui se contrôlait lentement, à la main. Le dépôt openai/math est public et consultable par tout le monde. Les prochains jours diront si des mathématiciens indépendants lancent réellement les vérifications Lean, et si les résultats annoncés tiennent sous ce contrôle. C'est de cette étape, plus que des chiffres, que dépendra la valeur du lot.
