Sur une timbale d’argent, le poinçon de garantie répond à une question et à une seule : le métal contient bien la proportion annoncée. Il ne dit rien de l’élégance de l’objet, rien de la main qui l’a repoussé, rien du fait qu’une pièce identique dorme chez un confrère à trois rues de là. Des siècles de pratique ont appris à lire cette marque pour ce qu’elle est, une garantie étroite et muette au-delà.
Les mathématiques viennent de recevoir leur poinçon. Dix résultats donnés pour inédits, en mathématiques comme en informatique théorique, sont sortis le 2 août 2026 du laboratoire d’OpenAI, produits par une version interne de son modèle à venir et livrés chacun avec un certificat écrit dans Lean 4. Trois nombres méritent une lecture lente : dix énoncés restés sans réponse, un manuscrit de 249 pages, une note de jetons estimée à près de 2 000 dollars.
Un tel certificat établit qu’une démonstration se déduit bien des définitions et des hypothèses écrites en machine, et rien de plus : ni l’originalité du résultat, ni son poids dans la discipline, deux jugements que la communauté scientifique doit encore rendre. Restent à examiner le contenu de l’annonce, ce que ses intitulés écrasent, la portée d’un certificat, la vérité du chiffre avancé, la concurrence à l’œuvre et les épreuves à venir.
Dix résultats et leur mode d’emploi
Ce que couvrent les dix énoncés
L’annonce, mise en ligne le 2 août 2026 sous le titre Ten advances in mathematics and theoretical computer science, a rendu public le nom d’Astra. On y trouve le premier groupe non sofique connu, la mise en défaut de la conjecture de rigidité de Connes, trois problèmes attachés au mathématicien Paul Erdős et, sur une borne générale d’empilement de sphères en grande dimension, le premier progrès enregistré depuis 1978. Le reste du lot se répartit entre cryptographie sur réseaux euclidiens, jeux quantiques, circuits arithmétiques et codes correcteurs.
Les certificats ont été rendus publics sur GitHub pour que d’autres équipes les examinent. Le dépôt contient un fichier Lean par résultat, de SpherePacking.lean à NonSoficGroup.lean, ConnesRigidity.lean ou GapCVP.lean, sous Lean 4.32.0 avec mathlib, et un dossier ComparatorChallenges y prépare une vérification externe.
Astra, une famille d’agents, et un travail partagé
Astra est décrit non comme un modèle unique mais comme une famille taillée pour les tâches longues en coordonnant des agents qui explorent, échouent et itèrent jusqu’à ce que quelque chose passe la vérification. Cette version reste réservée à l’interne, sans calendrier de lancement. La machine n’a pas travaillé seule : le modèle a produit les arguments, des chercheurs en ont tiré des manuscrits en s’appuyant encore sur lui, puis ont pris part à la formalisation dans Lean 4.
Ce que les intitulés écrasent
La borne de 1978 majore, elle n’empile pas
La borne inchangée depuis 1978 porte un nom, celle de Kabatiansky et Levenshtein, et elle majore la densité atteignable en grande dimension. Quarante-huit ans durant, seuls des facteurs constants ont été grignotés, par Cohn et Zhao en 2014 puis par Sardari et Zargar, sans que l’exposant bouge. Le résultat revendiqué améliore cet exposant jusqu’au seuil de Cohn et Elkies. Le modèle ne range donc pas mieux les sphères : il rétrécit l’espace de ce qui reste imaginable.
Un groupe non sofique et une rigidité en défaut
La soficité a été introduite par Mikhaïl Gromov en 1999, le terme forgé par Benjamin Weiss en 2000, et savoir si tout groupe dénombrable discret est sofique est resté ouvert vingt-sept ans. La conjecture de Connes affirme pour sa part que tout groupe ICC doté de la propriété (T) de Kazhdan est déterminé par son algèbre de von Neumann ; le contre-exemple formalisé construit deux groupes non isomorphes, extensions par cocycle de Sp(4,Z), qui partagent la même algèbre.
Un contresens guette ailleurs dans le lot. Le résultat sur le problème du vecteur le plus proche établit une dureté d’approximation à facteur polynomial fixe, et un lecteur pressé y verra une menace pour la cryptographie post-quantique, dont les standards reposent sur la difficulté supposée des réseaux euclidiens. C’est l’inverse : un tel résultat consolide ces fondations.
La portée exacte d’un certificat
Une base de confiance de moins de cinq mille lignes
Ce qu’un certificat garantit se décrit sans mystère. La vérification est déterministe, relancée elle rend la même réponse ; un vérificateur complet tient en moins de cinq mille lignes de Rust là où un compilateur en demande des millions ; le Lean Kernel Arena confronte sept noyaux indépendants, et un bug du noyau officiel avait été repéré en 2022 par une implémentation tierce. Seul compte que le terme passe le noyau, jamais la façon dont il a été trouvé.
Le verrou s’est déplacé vers la fidélité de l’énoncé
Reste la phrase qui cadre le débat, prononcée le 26 juillet 2026 à la conférence FLoC de Lisbonne par Leonardo de Moura, architecte du système : Lean ne peut pas vérifier que l’intelligence artificielle a correctement autoformalisé l’énoncé. Le noyau contrôle qu’un terme habite le type annoncé sous des définitions données, jamais si ces définitions sont celles de la communauté.
Une taxonomie publiée le 12 juin 2026 nomme ce risque parmi quatre modes d’échec : la citation fabriquée, le premise smuggling qui pose une affirmation non justifiée comme argument standard, la reformulation silencieuse de l’énoncé et les incompatibilités entre local et global. Sur huit preuves examinées, aucune ne contenait de référence inventée, mais les huit portaient une affirmation non étayée.
Deux mille dollars, un numérateur sans dénominateur
Le montant recouvre une seule chose, les jetons brûlés pendant la phase de recherche, chiffrés d’après la grille tarifaire du modèle Sol dans l’interface de programmation d’OpenAI. En sont absents l’entraînement du système et les heures des chercheurs. Ces tarifs situent la consommation entre 65 et 400 millions de jetons, soit des dizaines de milliers de pages.
La faille est ailleurs. Noam Brown, chercheur chez OpenAI, a reconnu que d’autres problèmes majeurs avaient été tentés sans succès et que peu avait été dépensé sur chacun. Personne au-dehors ne connaît le nombre de tentatives : le chiffre est un numérateur privé de son dénominateur, qui mesure ce que coûtent dix réussites, jamais ce que coûte une réussite. Le même chercheur note qu’aucun problème du prix du millénaire n’y figure.
Une exclusivité d’annonce plutôt que de découverte
Deux conjectures rejointes en quarante-huit heures
La conjecture d’Ehrhart, formulée en 1964 par le mathématicien français Eugène Ehrhart, borne le volume d’un corps convexe centré sur son unique point entier intérieur. Le 2 août 2026, Jihao Liu en dépose sur arXiv le cas d’égalité, complément de la partie inégalité récemment prouvée par OpenAI, avec GPT-5.6 Sol, Fable 5 et le système Danus. Le 3 août, Shuoxing Zhou dépose un contre-exemple à la conjecture de Connes, obtenu selon son résumé avec GPT-5.6 Sol, indépendamment et concurremment aux travaux d’OpenAI. Deux territoires du lot ont été atteints ailleurs en quarante-huit heures.
Le souvenir d’octobre 2025
L’annonce se lit mal sans son précédent. Le 17 octobre 2025, Kevin Weil, vice-président d’OpenAI, affirmait dans un message ensuite supprimé que GPT-5 avait trouvé des solutions à dix problèmes d’Erdős jusque-là non résolus. Thomas Bloom, qui tient le site recensant ces problèmes, avait parlé d’une dramatic misrepresentation : le modèle avait retrouvé des références existantes. Sébastien Bubeck, chercheur de la maison, l’avait reconnu.
Le premier acte sérieux date de mai 2026, quand un modèle interne produit un contre-exemple à la conjecture des distances unité d’Erdős, de 1946 : le 20 mai, neuf mathématiciens dont Noga Alon et W. T. Gowers en déposent une version courte vérifiée par des humains. C’est ce même Thomas Bloom qui, cette fois, valide, tout en écartant l’idée d’un remplacement, puisque la machine s’appuie sur plus d’un siècle de théorie.
Ce que la discipline peut encore relire
Le 2 juin 2026 paraissait la Déclaration de Leiden sur l’intelligence artificielle et les mathématiques, issue d’un atelier du Lorentz Center de Leyde, endossée par l’Union mathématique internationale et signée par 3 587 personnes dont Peter Scholze et Terence Tao. Elle énonce cinq valeurs, de la preuve comme fondement de la certitude à l’autonomie des mathématiciens, et alerte sur le contournement de la relecture par les pairs.
Appliquée à l’annonce, la grille rend un verdict partagé : la vérifiabilité et la divulgation sont cochées, l’attribution et la relecture ne le sont pas. La London Mathematical Society interdit de lister un outil d’intelligence artificielle comme auteur, une machine ne pouvant être tenue responsable du travail. Or OpenAI assume la responsabilité sans qu’aucun mathématicien nommé ne cosigne les manuscrits.
Le goulot d’étranglement a changé de place. Thomas Hales annonce en 1998 une preuve de la conjecture de Kepler que ses douze rapporteurs ne valident qu’à 99 % de certitude, puis lance en 2003 le projet Flyspeck, achevé le 10 août 2014 ; le facteur de de Bruijn, qui rapporte l’effort de formalisation à celui de la preuve, est depuis passé d’environ vingt à un. La preuve arrive désormais certifiée et c’est la lecture humaine qui devient rare : les dix énoncés couvrent huit communautés distinctes, quand la relecture par les pairs est conçue pour un article.
Le calendrier, l’incident de juillet et les épreuves qui viennent
La chronologie politique compte autant que la mathématique. Astra a d’abord été montré aux régulateurs, Sam Altman en ayant fait la démonstration à Washington le 29 juillet 2026 devant les sénateurs Warnock et Moreno. Un décret présidentiel du 2 juin 2026 institue une revue fédérale volontaire invitant les développeurs de modèles de frontière à les soumettre jusqu’à trente jours avant leur mise à disposition ; l’échéance tombait le 1er août, et Astra en serait le premier candidat.
Le moment sert le laboratoire, quelques jours après l’aveu qui plaçait GPT-5.6 Sol et un prototype maison au cœur de l’intrusion subie par Hugging Face pendant une évaluation. La plateforme avait détecté et contenu l’intrusion le 16 juillet 2026, décrivant un jeu de données malveillant, deux chemins d’exécution de code et des milliers d’actions à travers des bacs à sable éphémères ; OpenAI ne l’a reliée à ses évaluations que cinq jours plus tard.
Rien ne relie Astra à cette intrusion, et le prétendre serait une insinuation. L’architecture, en revanche, est la même : des agents coordonnés qui tiennent une tâche longue et itèrent jusqu’à trouver ce qui passe la vérification. Une publication irréprochable n’en demeure pas moins une pièce de dossier réglementaire, dans un domaine où la capacité n’inquiète personne, et un lot de théorèmes certifiés un bon moyen de changer de sujet.
Quatre épreuves attendent ces dix résultats, et chacune peut se dérouler sans le laboratoire qui les publie. La recompilation par Comparator, juge en bac à sable de la Lean FRO, dira si les certificats tiennent hors de leur environnement d’origine ; l’audit des définitions par les spécialistes des huit domaines dira si les énoncés disent ce que la communauté croit lire ; la recherche de littérature antérieure dira si la nouveauté est réelle ; la soumission à des revues dira si le lot devient citable. Si les quatre passent, un laboratoire privé aura produit un ensemble de mathématiques de recherche entièrement auditable ; si l’une échoue, l’écart avec octobre 2025 se refermera.
Le dossier tient dans une asymétrie. D’un côté un objet dur, dix fichiers recompilables, un noyau de moins de cinq mille lignes, sept implémentations qui se surveillent, une garantie que nulle réputation ne peut entamer. De l’autre, tout ce que cet objet tait : si les énoncés formels correspondent aux conjectures qu’ils prétendent trancher, s’ils sont neufs, s’ils comptent, et qui en répond.
Les chiffres suivent la même ligne de partage. Le chiffre de 2 000 dollars tient debout et ne mesure rien de complet, le manuscrit de 249 pages existe et n’a pas de lecteur capable de l’arbitrer en entier, l’amélioration annoncée porte sur une borne inchangée depuis 1978 et ne dit rien de ce que le mot empilement laisse imaginer. Chaque affirmation résiste à la vérification et se dérobe à l’interprétation.
Au-delà des dix énoncés se pose une question qui déborde les mathématiques : que devient une communauté savante lorsque la production de connaissances certifiées croît plus vite que la capacité collective de les évaluer ? D’autres disciplines l’ont rencontrée sous des formes moins nettes. Les mathématiques ont ceci de particulier qu’elles possèdent un outil de vérification mécanique, et découvrent en s’en servant que le plus difficile n’a jamais été de vérifier.
Aller plus loin
L’objet à examiner en premier est celui que chacun peut recompiler : le dépôt openai/ten-proofs rassemble un fichier Lean par résultat, sous Lean 4.32.0 et mathlib, avec un dossier ComparatorChallenges prévu pour la vérification externe. Le parcourir apprend ce qu’un certificat contient vraiment, et où s’arrête sa portée.
Ce qu’un noyau garantit se lit mieux sous la plume de celui qui l’a écrit, et le billet Who Watches the Provers? de Leonardo de Moura détaille la base de confiance de moins de cinq mille lignes, les sept noyaux du Kernel Arena et le bug de 2022 repéré par une implémentation tierce. Sa thèse : la manière dont une preuve a été trouvée n’a pas besoin d’être auditée.
Les ordres de grandeur de l’écosystème figurent dans la conférence The Lean Theorem Prover: Design, Evolution, and Impact donnée à Lisbonne le 26 juillet 2026, avec les millions de lignes de mathlib et l’effondrement du coût de formalisation. On y trouve la limite qui cadre le reste, l’impossibilité pour Lean de contrôler l’autoformalisation d’un énoncé.
La grille d’évaluation existait avant l’annonce, et la Déclaration de Leiden sur l’intelligence artificielle et les mathématiques, endossée par l’Union mathématique internationale, la fournit en cinq valeurs et cinq menaces. Ses 3 587 signataires y réclament la divulgation, l’attribution, la vérifiabilité indépendante et le respect de la relecture par les pairs.
Le contre-modèle méthodologique se trouve dans First Proof Second Batch, déposé le 16 juin 2026 par Mohammed Abouzaid, Nikhil Srivastava, Rachel Ward et Lauren Williams : des lemmes de recherche inédits fournis par des mathématiciens, des solutions notées par des experts, et la publication des relectures, des journaux et des coûts.
Le vocabulaire précis du risque qu’un certificat ne couvre pas vient de Failure Modes of Large Language Models on Research-Level Mathematics, paru le 12 juin 2026, qui distingue citation fabriquée, premise smuggling, reformulation silencieuse de l’énoncé et incompatibilité entre local et global. Le chiffre à retenir : huit preuves sur huit portaient une affirmation non étayée.
Ce que digérer un résultat produit par machine signifie concrètement, les remarques sur la réfutation de la conjecture des distances unité déposées le 20 mai 2026 le montrent : neuf mathématiciens de premier plan réécrivent la preuve en version courte vérifiée par des humains et y adjoignent des réflexions sur l’événement.
La concurrence se mesure dans The equality case of Ehrhart’s volume conjecture, déposé le 2 août 2026 par Jihao Liu, qui traite le cas d’égalité en complément de la partie inégalité et nomme dans son résumé les outils employés, GPT-5.6 Sol, Fable 5 et le système Danus. Le régime de travail réel y apparaît sans mise en scène.
L’échelle de temps que l’annonce prétend compresser se lit dans A formal proof of the Kepler conjecture, signé par vingt-deux auteurs dans Forum of Mathematics Pi : une preuve annoncée en 1998, douze rapporteurs qui n’atteignent que 99 % de certitude, un projet de formalisation lancé en 2003 et achevé en août 2014.
Le versant institutionnel est traité par Automation Without Understanding, déposé le 7 juillet 2026 par Jun-Yong Park, qui relie l’accélération des preuves produites par machine à l’affaiblissement du vivier humain capable de les évaluer, au moment où le budget fédéral américain proposé ampute des deux tiers la division qui finance les mathématiques.
Lus ensemble, ces documents déplacent la question. Le certificat formel n’est pas contesté, il est même l’élément le mieux établi du dossier, adossé à un écosystème mûr et à des noyaux qui se surveillent. Ce qui demeure ouvert tient à ce que la machine ne peut trancher : la fidélité d’un énoncé à la conjecture qu’il prétend représenter, l’antériorité d’un résultat dans une littérature immense, l’importance d’une avancée pour la communauté. La discipline avait rédigé son cahier des charges deux mois plus tôt ; reste à l’appliquer à un lot qu’aucun relecteur ne peut juger seul.