OpenAI : dix résultats mathématiques formalisés en Lean, le rôle du modèle interne

Le 1er août, OpenAI a publié le manuscrit « Ten Advances in Mathematics and Theoretical Computer Science » en attribuant les résultats à l'un de ses modèles internes. Dans le même temps a été créé le dépôt GitHub `openai/ten-proofs`, qui met à disposition les formalisations Lean 4 des dix démonstrations. Parmi les résultats, on remarque l'amélioration de l'exposant pour l'empilement de sphères — la première depuis 1978 —, la construction d'un groupe non sofique et un contre-exemple à la conjecture de rigidité de Connes. Le dépôt est un projet Lean 4.32.0 fondé sur mathlib, publié sous licence Apache-2.0 : n'importe qui peut recompiler les démonstrations avec `lake exe cache get` et `lake build All`, et un dossier ComparatorChallenges explique comment mener la vérification de façon indépendante.

La presse a relié ces résultats à « Astra », le nom de la prochaine famille de modèles annoncée par OpenAI ce même 1er août ; le manuscrit, lui, ne parle que d'« un modèle interne », non publié. Des données comme le coût d'environ 2 000 dollars en tokens ou les 249 pages du document proviennent d'articles tiers, la page d'annonce officielle étant actuellement inaccessible. L'article remercie des mathématiciens humains pour la relecture et signale un travail indépendant et concomitant de Shuoxing Zhou, mené en partie avec l'aide de GPT-5.6 Sol.

Selon SiliconANGLE, les arguments mathématiques viennent du modèle, mais ce sont des chercheurs humains qui ont transformé sa production en manuscrits publiables : le poids de cette mise au point n'est pas quantifié. L'usage de Lean 4 déplace le débat : si le certificat garantit la validité logique de la démonstration, il ne confirme pas automatiquement que l'énoncé formalisé coïncide avec le problème ouvert historique, contrôle qui reste du ressort humain. Aucun des dix résultats n'a passé de relecture par les pairs formelle. Le précédent pèse : en octobre 2025, l'annonce de dix problèmes d'Erdős « résolus » par GPT-5 s'est révélée infondée, et Thomas Bloom, qui tient erdosproblems.com, y a vu une grave présentation erronée. Sur les dix résultats d'aujourd'hui, le même Bloom parle en revanche de « big news ». Comme le note le physicien théoricien Tobias J. Osborne, les 2 000 dollars cités correspondent au coût des tokens gagnants, pas à la récolte totale des tentatives — une donnée sur laquelle OpenAI n'a rien communiqué. Ce scénario s'inscrit dans le contexte de la « Leiden Declaration on Artificial Intelligence and Mathematics », publiée en juin 2026 et soutenue, selon the-decoder, par plus de 3 000 mathématiciens et par l'International Mathematical Union, qui réclame transparence, protection des droits des auteurs et responsabilité humaine sur les résultats.

La vraie nouvelle n'est pas qu'une machine ait fait des mathématiques — cela arrive depuis des mois — mais que cette fois chaque résultat arrive avec un certificat Lean recompilable : pour juger, nul besoin de faire confiance à celui qui annonce. Tant que le rapport entre tentatives ratées et réussites restera un secret industriel, évaluer l'efficacité de ces modèles demeurera pourtant un exercice de foi plus que de statistique.