Le 1er août 2026, OpenAI a annoncé qu’une version interne de son prochain modèle, nommée Astra, présentait de nouveaux résultats sur dix problèmes ouverts de mathématiques et d’informatique théorique. Ces problèmes étaient ouverts depuis au moins dix ans. Le résultat mis en avant est la première construction explicite d’un groupe non sofique, une question centrale de la théorie des groupes depuis que Mikhail Gromov a introduit la notion de soficité en 1999.
Un point de vocabulaire avant tout le reste : Astra est un modèle interne, non publié. Personne à l’extérieur d’OpenAI ne peut l’exécuter. Ce qui a été rendu public, ce ne sont pas les capacités du modèle, ce sont ses sorties. Cette distinction structure tout ce qui suit.
La plupart des articles parus depuis tiennent dans un titre : une IA résout des problèmes de mathématiques restés ouverts. C’est ce qu’OpenAI présente, et c’est la partie la moins informative. La question utile est autre : par quel mécanisme sait-on que ces résultats tiennent, et à quel endroit exact ce mécanisme cesse de garantir quoi que ce soit.
Ce qui a été publié
OpenAI a déposé sur GitHub, sous licence Apache 2.0, trois choses distinctes qu’il vaut mieux ne pas confondre :
- Un manuscrit de 249 pages, soit l’exposé en mathématiques rédigées, lisible par un humain.
- Les traces de raisonnement du modèle, soit le chemin suivi pour arriver là.
- Des certificats de preuve en Lean 4, soit des fichiers dont la validité se contrôle par logiciel.
Les domaines couverts vont de la théorie des groupes aux algèbres de von Neumann, en passant par la géométrie en grande dimension, la complexité quantique, la cryptographie sur réseaux euclidiens et la combinatoire extrémale. OpenAI indique par ailleurs qu'Astra aurait résolu trois problèmes associés au mathématicien Paul Erdős.
Ce que « sorry à zéro » veut dire
Lean est un langage dans lequel une démonstration s’écrit comme un programme, et se contrôle comme un programme : soit le fichier passe le vérificateur, soit il ne passe pas. Le mot-clé sorry y sert d’échappatoire. Il marque une étape que l’auteur n’a pas démontrée et demande au vérificateur de l’admettre pour continuer. C’est commode pendant la rédaction, et c’est exactement ce qui vide une preuve de sa valeur si on l’oublie dedans.
Le dépôt publié affiche un compteur de sorry à zéro. Autrement dit, aucune étape de la formalisation n’est laissée en suspens. Pas de trou déclaré, pas de lemme admis en cours de route, pas d’endroit où la chaîne se repose sur la bonne foi du lecteur. C’est un détail technique qui ressemble à une note de bas de page, et c’est en réalité l’information la plus solide de toute l’annonce.
Pourquoi une preuve vérifiée par machine change la nature de l’affirmation
Le reproche adressé aux modèles de langage en mathématiques est connu : ils produisent des démonstrations qui se lisent bien et qui sont fausses. Une étape sautée, un cas particulier traité comme le cas général, une référence à un théorème qui ne dit pas tout à fait ça. Le texte a la forme d’une preuve sans en avoir la fonction, et il faut un relecteur compétent pour repérer où la chaîne casse.
Le format Lean déplace ce problème. Quand une preuve est acceptée par le vérificateur, sa validité ne dépend plus de la fiabilité du modèle qui l’a produite, ni de l’attention du relecteur qui la lit. Elle dépend d’un logiciel indépendant du modèle, que n’importe qui peut faire tourner sur les fichiers publiés. Une affirmation passée au contrôle mécanique n’est pas une affirmation de modèle de langage un peu meilleure : c’est un objet d’une autre nature.
Thomas Bloom, mathématicien à l’Université de Manchester, tient le catalogue des problèmes d’Erdős. Il a qualifié les résultats de « big news » sur X. Venant de quelqu’un dont le travail consiste précisément à savoir ce qui est ouvert et ce qui ne l’est plus, la remarque pèse davantage qu’un commentaire général sur les progrès de l’IA.
La limite dont presque personne ne parle
Voici l’endroit exact où la garantie s’arrête, et il est plus étroit que ce qu’on lit généralement.
Une compilation Lean réussie établit une chose et une seule : la démonstration est valide pour le théorème tel qu’il est formulé dans le fichier Lean. Elle n’établit pas que cet énoncé formel capture le problème ouvert tel que la communauté mathématique le comprenait. Ce sont deux affirmations différentes, et la seconde n’est pas mécanisable.
Entre le problème ouvert, formulé dans la langue et les conventions d’un domaine, et le théorème écrit en Lean, il y a un acte de traduction. Cet acte est humain. Il suppose de choisir des définitions, de fixer des quantificateurs, de décider ce qui est hypothèse et ce qui est conclusion. Une formalisation peut être parfaitement correcte et légèrement plus faible que le problème visé. Elle peut aussi porter une hypothèse supplémentaire qui rend l’énoncé vrai mais moins intéressant. Le vérificateur n’a rien à dire là-dessus : il ne connaît que le fichier qu’on lui donne.
Cette limite compte particulièrement ici, parce que des chercheurs extérieurs relèvent que du personnel d’OpenAI a participé à la préparation des articles et à la formalisation des arguments. La traduction du problème ouvert vers l’énoncé Lean, c’est-à-dire précisément l’étape que la machine ne certifie pas, a donc été faite du côté de l’organisation qui annonce le résultat. Ce n’est pas une accusation, c’est une description de la répartition des rôles. Elle indique où devra porter l’examen des mathématiciens dans les mois qui viennent : pas sur les preuves, qui passent le vérificateur, mais sur les énoncés.
À ce jour, la communauté n’a pas statué sur l’équivalence entre les énoncés formalisés et les problèmes ouverts correspondants. C’est le point en suspens, et c’est celui qu’il faut garder en tête en lisant « dix problèmes résolus ».
Vérifiable ne veut pas dire reproductible
Deux mots circulent comme s’ils étaient interchangeables. Ils ne le sont pas, et la différence est ici tout le sujet.
Vérifier, c’est reprendre les certificats publiés et les repasser au contrôleur Lean. N’importe qui peut le faire, aujourd’hui, avec les fichiers du dépôt. C’est ce qui rend cette annonce moins invérifiable que la moyenne des annonces du secteur.
Reproduire, c’est refaire tourner le procédé qui a produit ces certificats et obtenir des résultats du même ordre. Personne à l’extérieur ne peut le faire, puisque le modèle n’est pas accessible. Le résultat peut donc être vérifié, il ne peut pas être reproduit.
La conséquence est nette. Ce qui est établi, c’est que ces dix théorèmes, tels que formalisés, tiennent. Ce qui n’est pas établi, c’est qu’un modèle produise ce type de résultat de façon régulière, ni qu’un autre laboratoire obtiendrait quoi que ce soit de comparable avec une méthode voisine. La première affirmation porte sur des théorèmes, la seconde sur une capacité. Seule la première est démontrée.
Ce que 2 000 dollars veut dire, et ne veut pas dire
Le chiffre qui a le plus circulé est celui du coût : environ 2 000 dollars de calcul. Il est frappant, et il est mal lu presque partout.
Ce montant couvre les exécutions réussies, pas l’ensemble des tentatives du modèle. C’est donc un coût de publication, pas un coût de découverte. La distinction n’est pas rhétorique, elle change l’ordre de grandeur de ce qu’on peut en déduire : on connaît le prix des billets gagnants, on ne connaît pas le nombre de billets achetés.
S’y ajoute le fait qu’OpenAI a choisi quels résultats publier. On ignore combien de problèmes ont été attaqués, combien sont restés sans réponse, combien ont produit une formalisation qui n’a pas passé le vérificateur. Sans ce dénominateur, le taux de réussite du procédé n’est pas calculable, et 2 000 dollars ne dit rien du coût du résultat suivant.
Le chiffre garde un intérêt, plus modeste : il indique qu’une fois le résultat obtenu, le formaliser et le publier ne coûte pas grand-chose. Dans un mois où OpenAI a ramené le prix d’entrée de GPT-5.6 Luna à 0,20 dollar par million de tokens, soit 80 % de moins, cette baisse du prix affiché est bien réelle. Elle ne dit toujours rien du coût d’un résultat.
Ce qu’un dirigeant peut en retenir sans extrapoler
Trois enseignements tiennent. Le quatrième point n’en est pas un, c’est une abstention.
Le premier concerne la nature du domaine. Ce qui a fonctionné ici a fonctionné dans un domaine où la correction est mécaniquement contrôlable. Les mathématiques formalisées ont cette propriété rare : il existe un juge qui n’a pas d’avis. Presque aucun problème d’entreprise n’a cette structure. Un plan commercial, un positionnement, un arbitrage de priorités n’ont pas de compilateur. Transposer directement les performances observées en mathématiques vers ces sujets n’a aucun fondement.
Le deuxième est transposable, lui. Le principe utile n’est pas que le modèle est fort, c’est qu’un modèle devient fiable quand on place un vérificateur entre sa sortie et la décision. En développement logiciel, ces vérificateurs existent déjà et coûtent peu : typage strict, tests automatisés, compilation, revue de code, intégration continue. C’est ce mécanisme, et lui seul, qui transforme une production de modèle en production exploitable. C’est aussi la raison pour laquelle nos prestations de développement n’intègrent pas de code généré sans chaîne de contrôle, quel que soit le modèle qui l’a écrit.
Le troisième porte sur la lecture des annonces. Devant une communication de laboratoire, la bonne question n’est plus de savoir ce que le modèle a fait, mais ce qu’un tiers peut contrôler et ce qu’il doit croire sur parole. Ici : les preuves sont contrôlables, les énoncés sont à examiner, le procédé est à croire sur parole. Cette grille se réapplique telle quelle à l’annonce suivante, et il y en aura une.
Le quatrième point est donc une abstention. Ces résultats ne permettent aucune conclusion sur les délais. Gary Marcus le relève : aussi notables soient-ils, ils n’établissent ni une intelligence artificielle générale ni l’arrivée prochaine d’un résolveur universel. Dix théorèmes formalisés sont dix théorèmes formalisés.
Ce qui est établi, ce qui ne l’est pas
Établi : les certificats Lean 4 sont publics, sous licence Apache 2.0, sans aucun sorry, et n’importe qui disposant de Lean peut les recontrôler. Le manuscrit de 249 pages et les traces de raisonnement sont là. Sur le plan de la vérifiabilité, le dossier est donc contrôlable pièce par pièce.
Non établi : que les énoncés formels correspondent aux problèmes ouverts tels que la communauté les comprend, qui reste la question ouverte du dossier. Que le procédé soit reproductible ailleurs. Que 2 000 dollars mesure le coût d’une découverte. Que ces résultats indiquent quoi que ce soit sur un système général.
La position raisonnable n’est ni l’enthousiasme ni le scepticisme de principe. Elle consiste à savoir, pour chaque pièce du dossier, à quelle question elle répond et laquelle elle laisse ouverte. Un vérificateur mécanique répond à une question très précise, très bien. C’est déjà beaucoup, et ce n’est pas tout.
Si vous voulez examiner comment ce type de garde-fou s’applique à un projet en cours, décrivez-nous votre contexte. Nous travaillons par écrit et répondons sous 24 heures ouvrées.
