Le chiffre qui compte est 460 000 : les lignes de preuve formellement vérifiable qu'OpenAI a déposées dans un dépôt GitHub public le 1er août pour étayer dix avancées revendiquées en mathématiques et en informatique théorique. Le billet qui les annonce, daté du même matin, dit que les résultats viennent d'une version interne d'Astra, 'notre prochain modèle majeur'. Chacun des dix résultats est accompagné d'un certificat Lean, une preuve formelle vérifiable par machine, dans le dépôt github.com/openai/ten-proofs sous licence Apache-2.0. Nous avons vérifié les fichiers : les dix compilent avec Lean 4.32 et mathlib, et aucun ne contient de 'sorry' ni d'axiome sur mesure, les deux portes de sortie habituelles.

Les dix, tels qu'OpenAI les énonce : de nouvelles bornes supérieures pour l'empilement de sphères en haute dimension jusqu'au seuil de Cohn-Elkies ; des bornes exponentiellement améliorées pour les codes binaires et sphériques ; une construction de groupes non sofiques ; un contre-exemple réfutant la conjecture de rigidité de Connes ; des bornes inférieures pour le permanent, dont une borne de formule arithmétique d'ordre n puissance quatre sur log n ; un théorème de répétition parallèle exponentiel pour les jeux quantiques ; une dureté d'approximation à facteur polynomial pour le problème du vecteur le plus proche ; une réponse précise à la conjecture de volume d'Ehrhart ; une borne inférieure superexponentielle pour les nombres de Ramsey multicolores du triangle, qui trancherait le problème d'Erdős 183 ; et des contre-exemples aux conjectures de compacité et de dégénérescence, tranchant les problèmes d'Erdős 146 et 180. Selon OpenAI, chaque problème était bloqué depuis au moins dix ans. Ce cadrage est le leur, comme le chiffre d'environ 2 000 dollars de calcul aux tarifs Sol de l'API.

Voici ce qui est vérifiable indépendamment aujourd'hui, et c'est plus que rien et moins qu'une preuve. Vérifiable : le dépôt existe, les dix fichiers Lean y sont, leur contenu est tel que décrit, deux PDF compagnons (l'article et les narrations de raisonnement du modèle) se téléchargent, et le dépôt inclut des configurations pour une vérification par un noyau indépendant. Pas encore vérifiable : personne hors d'OpenAI n'a dit avoir reconstruit les preuves ; aucun mathématicien humain ne les a évaluées ; et aucun expert ne confirme que les énoncés formalisés disent ce que disent les théorèmes informels, l'étape où la formalisation peut casser en silence. Le signal le plus fort de non-ratification : erdosproblems.com, le traqueur de référence, liste encore le problème 183 comme ouvert avec un prix de 250 dollars, tandis qu'un traqueur plus petit l'a déjà marqué résolu le 1er août. Thomas Bloom, qui maintient ce site, a parlé de 'grande nouvelle' et de 'gros' pour les constructions, dans des messages cités par The Decoder ; nous n'avons pas pu les récupérer directement.

Sur le nom, la précision compte parce que c'est l'article que les gens vont citer. Le billet dit 'une version interne d'Astra, notre prochain modèle majeur'. L'expression 'prochaine grande famille de modèles' vient du chercheur d'OpenAI Noam Brown, qui a ajouté 'hélas pas de problèmes du Millénaire (pas encore)', et note que le modèle a échoué sur d'autres grands problèmes. Tout le reste est rapporté, pas confirmé : The Information, via The Decoder, place Astra comme une nouvelle classe à côté de Sol, Terra et Luna, la décision GPT-6 contre GPT-5.7 étant non tranchée et sans date de sortie. La note d'éthique d'OpenAI mérite d'être citée entière : 'revendiquer la paternité humaine d'une preuve entièrement générée par un système d'IA présenterait mal la contribution du système et la nature du travail intellectuel humain authentique', et l'entreprise dit assumer la responsabilité de la justesse pendant que les arguments étaient générés par le modèle. C'est la phrase à laquelle la tenir quand les reconstructions arriveront.