L’essentiel
- OpenAI a publié le 6 octobre 722 manuscrits de mathématiques, répartis en 372 ensembles de résultats, produits par un modèle interne non publié.
- Beaucoup de preuves sont accompagnées d’une formalisation en Lean, un langage qui permet à un ordinateur de vérifier chaque étape ; d’autres formalisations doivent suivre.
- Le dépôt GitHub chiffre le coût (en moyenne l’équivalent de trois heures de réflexion de ChatGPT Pro par résultat), mais les chercheurs extérieurs ne peuvent pas essayer le modèle.
OpenAI a déposé d’un coup sur GitHub 722 manuscrits de mathématiques, tous issus d’un modèle que personne hors du laboratoire ne peut interroger. Le laboratoire revendiquait déjà en septembre plus de 100 problèmes ouverts résolus ; cette livraison change surtout le débit. À ce rythme, la production de résultats dépasse la capacité de les lire.
Des preuves Lean, mais pas pour tout
Lean est un langage de programmation dans lequel une preuve s’écrit de façon assez rigoureuse pour qu’une machine la vérifie ligne par ligne. OpenAI en joint pour « beaucoup » de ses démonstrations et promet de compléter le dépôt à mesure que d’autres formalisations seront obtenues. Une partie du lot reste donc, aujourd’hui, à la charge de relecteurs humains.
Même pour les preuves formalisées, la vérification mécanique répond à une seule question : le théorème écrit en Lean est-il démontré ? Elle ne dit pas si cet énoncé traduit fidèlement le problème que les mathématiciens se posaient. Cette traduction se relit à la main, et un énoncé légèrement trop faible peut passer le contrôle de la machine sans résoudre grand-chose.
Dix résumés de raisonnement pour 722 manuscrits
Le communiqué détaille ce qu’OpenAI ajoute au dépôt pour la transparence : 10 résumés du raisonnement du modèle, des estimations de calcul exprimées en usage de ChatGPT Pro, et des statistiques sur le nombre de problèmes tentés. Dix traces pour plus de sept cents manuscrits, cela éclaire quelques cas et laisse le reste dans l’ombre.
La donnée la plus précieuse est sans doute la plus discrète : le nombre de problèmes tentés. Avec lui, on peut rapporter les succès aux essais et mesurer un taux de réussite, au lieu d’admirer seulement les réussites. En revanche, l’unité de coût choisie, des heures de ChatGPT Pro, renvoie à un produit commercial et à un modèle que personne d’autre ne peut faire tourner : impossible de la reproduire.
Juger un modèle sans pouvoir l’interroger
Le modèle n’est pas publié. OpenAI dit travailler à une mise à disposition responsable, sans date. D’ici là, l’évaluation extérieure se réduit à lire des sorties choisies par le laboratoire : on ne peut ni lui poser un problème de son choix, ni rejouer un échec, ni vérifier que les 722 manuscrits ne sont pas le meilleur d’un tri.
Le comité consultatif indépendant sur les mathématiques et l’intelligence artificielle (AGMAI), hébergé par l’Institute for Advanced Study, avait formulé fin septembre ses premières recommandations : publier par des canaux académiques établis quand c’est possible, indiquer le nom du modèle, les prompts et les coûts de calcul, et ne pas se servir de ces résultats pour promouvoir un modèle. OpenAI dit s’en être inspiré. Le communiqué ne nomme pourtant pas le modèle et ne mentionne pas les prompts ; la diffusion passe par GitHub, avec des alternatives communautaires encore à l’étude.
Le coût humain apparaît aussi dans les commentaires. Sur Hacker News, un ancien passionné de théorie des graphes raconte avoir consacré 24 ans, par intermittence, à la conjecture de Barnette, dont la preuve figurerait désormais au problème 180 du dépôt. Il écrit ne pas savoir quoi en penser : des milliers d’heures de plaisir, et une tristesse diffuse d’apprendre qu’elle serait résolue. Cette réaction est une donnée de plus sur ce que l’on demande à la communauté d’encaisser.
Déléguer ce qu’un test peut trancher
Les mathématiques ont un avantage rare : un vérificateur automatique existe. Quand il couvre le résultat, un flux massif de productions d’IA peut être audité à la vitesse de la machine. Quand il manque, ou qu’il ne couvre qu’une partie, la qualité retombe sur des relecteurs dont le temps n’augmente pas avec la puissance de calcul.
Le même partage vaut pour le code, les contrats ou les analyses : ce qu’un test peut trancher se délègue, le reste demande des lecteurs. Si vous mettez des agents en production, demandez-vous moins ce qu’ils savent faire que ce qui vérifie leur travail, et sur quelle part. Le dépôt d’OpenAI montre ce dont ce contrôleur est capable, et ce qu’il laisse encore à lire.
Mon avis
Le calcul de ces résultats coûte quelques heures de machine chacun, leur lecture coûte le temps rare d’experts : le rapport ne fera que se creuser. Le premier lot dont une preuve Lean passera alors que l’énoncé formalisé trahit le problème posé obligera les laboratoires à ouvrir l’accès à leurs modèles, faute de quoi la communauté cessera de les lire.
Sources
Ils m’ont fait confiance
« Il ne se contente pas de corriger les symptômes, il cherche à comprendre l'origine des problèmes et à sécuriser les modifications effectuées. J'ai réellement le sentiment d'avoir trouvé un développeur qui comprend à la fois la technique et les enjeux globaux du projet. »
Évaluation client · projet WordPress · septembre 2026
5,0/5 sur 17 évaluations
Faire appel à mes services →
