Calipia : le blog

En plein mois d’aout dans le chaud estival en France, OpenAI a publié dix résultats mathématiques inédits, produits par une version interne de son futur modèle Astra. Parmi eux, la construction explicite d’un groupe non sofique, une question ouverte depuis que Mikhail Gromov a formalisé la notion de soficité en 1999. De quoi impressionner, à raison. Mais l’affaire a rapidement tourné à la polémique de paternité scientifique, puis à une réflexion plus large sur la manière dont les éditeurs d’IA communiquent leurs percées. Pour un DSI ou un RSSI qui doit chaque semaine trier le solide du marketing dans les annonces IA de ses fournisseurs, l’épisode vaut le détour. Il condense en un seul cas d’école à peu près tous les réflexes de vigilance que nous recommandons habituellement dans nos Briefings.

Ce qu’Astra a réellement produit

OpenAI a publié plus de 250 pages de manuscrits, 60 pages supplémentaires décrivant le cheminement du raisonnement, et surtout un certificat Lean pour chacun des dix résultats. Lean est un assistant de preuve qui contraint chaque étape d’un raisonnement mathématique à être vérifiable mécaniquement : aucune ligne ne peut être acceptée si elle ne découle pas logiquement de la précédente. Ce niveau de vérification formelle est une nouveauté à cette échelle pour une annonce IA, et c’est précisément ce qui a convaincu la majorité des mathématiciens interrogés que quelque chose de réel s’était produit, même ceux qui n’étaient pas en mesure d’évaluer personnellement chacun des dix résultats tant les domaines couverts (théorie des groupes, empilement de sphères en haute dimension, codes correcteurs d’erreurs, complexité quantique, cryptographie sur réseaux euclidiens) sont devenus hyperspécialisés.

Le mathématicien James Maynard, médaille Fields 2022 et professeur à Oxford, résume l’ampleur de l’exercice : résoudre l’un seul de ces dix problèmes suffirait généralement à décrocher un poste académique. Astra en a livré dix d’un coup. On comprend l’émoi.

Il faut cependant garder à l’esprit ce que Lean vérifie réellement, et ce qu’il ne vérifie pas. Un certificat Lean garantit la cohérence logique interne d’une démonstration. Il ne garantit pas que le problème a été formalisé de manière fidèle à ce que la communauté entendait par cet énoncé, ni que le résultat est aussi original que le communiqué le laisse entendre. Cette nuance, presque anodine en apparence, est au cœur de la controverse qui a suivi.

La dispute d’attribution, ou l’art de sous-peser ce qu’on doit aux autres

Le résultat le plus commenté, l’existence de groupes non sofiques, s’appuie en réalité sur des travaux publiés en 2016 et 2019 par Andreas Thom (université technique de Dresde) et Gábor Kun (institut Alfréd Rényi de Budapest). La formulation initiale d’OpenAI présentait ses résultats comme portant sur des problèmes n’ayant vu « aucun progrès sur le résultat principal depuis au moins une décennie ». Une phrase que Kun a jugée pour le moins maladroite, dans la mesure où l’article de recherche joint reconnaissait explicitement s’appuyer sur ses travaux de 2016 et 2019. OpenAI a depuis discrètement modifié la formulation de son annonce, sans note de correction ni explication publique du changement, pour indiquer que ses résultats « résolvent ou font progresser substantiellement » des problèmes ouverts de longue date.

Interrogée, l’entreprise a confirmé la modification et justifié qu’elle souhaitait mieux refléter les travaux préalables sur lesquels ses résultats s’appuient. Un correctif après coup, obtenu après un échange de courriels avec le chercheur concerné, plutôt qu’une transparence spontanée. D’autres chercheurs ont depuis pointé des schémas similaires sur d’autres résultats du lot, notamment sur l’amélioration de l’empilement de sphères qui reprendrait, sans attribution suffisante selon son auteur, un argument publié en 2016.

Pour qui suit de près la gouvernance de l’IA en entreprise, ce schéma est familier. Un communiqué maximaliste, une formulation qui gomme les contributions tierces, puis une correction discrète une fois la contestation devenue publique. C’est exactement le type de dérive que la Déclaration de Leyde sur l’usage responsable de l’IA en mathématiques, signée par plus de 3 400 chercheurs et endossée par l’Union mathématique internationale, cherche à endiguer en appelant les éditeurs à ne pas surjouer les capacités de leurs produits. On retrouve ici, dans un registre académique, les mêmes tensions que celles que l’article 4 de l’AI Act tente d’adresser côté entreprise : l’obligation de culture et de compréhension réelle des systèmes d’IA déployés, à rebours de la simple confiance en la communication du fournisseur.

Le prix affiché n’est pas le coût réel

OpenAI a mis en avant un chiffre choc : générer les dix solutions aurait coûté environ 2 000 dollars en tokens, au tarif API de son modèle Sol. Un montant dérisoire au regard de l’ampleur des résultats, et un excellent argument marketing sur la démocratisation de la recherche. Les mathématiciens consultés se montrent nettement plus circonspects sur ce chiffre. Il ne reflète que le coût des tentatives réussies, sans compter le nombre de problèmes tentés et abandonnés en cours de route, ni les itérations nécessaires pour arriver à un résultat exploitable. Autrement dit, un coût de succès, pas un coût de recherche.

Cette distinction devrait résonner chez tout DSI qui a déjà comparé un TCO d’infrastructure IA annoncé par un éditeur à la facture réelle une fois intégrés les essais infructueux, le fine tuning, la relecture humaine et la gouvernance associée. Le chiffre publié dans une slide de lancement et le coût total de possession sont rarement le même nombre, en mathématiques comme en salle de conseil.

Accès et souveraineté : un débat qui ne concerne pas que les mathématiciens

Autre point de friction : l’accès inégal aux modèles les plus capables. OpenAI et Anthropic proposent des programmes gratuits pour les chercheurs académiques, mais peu des mathématiciens interrogés par nos confrères de The Vergeavaient pu réellement mettre la main sur les systèmes les plus avancés avant leur publication grand public. James Maynard et Colva Roney-Dougal, professeure à l’université de St Andrews, expriment tous deux l’espoir que des modèles à poids ouverts puissent un jour combler cet écart d’accès, plutôt que de dépendre d’une poignée d’acteurs commerciaux.

C’est un débat que nous suivons de près à Calipia sous l’angle de la souveraineté numérique européenne, et il s’exprime ici presque à l’identique : une poignée d’entreprises américaines contrôle l’accès aux capacités de pointe, avec toutes les questions de dépendance stratégique, de coût d’accès et de gouvernance des données que cela suppose, y compris pour un champ aussi peu commercial en apparence que la théorie des groupes.

Ce que Roney-Dougal appelle une « cour de récréation publicitaire »

La formule est sévère mais éclairante. Roney-Dougal reproche aux entreprises d’IA de traiter une discipline entière comme un terrain de démonstration commerciale, avec toute l’incitation qui va avec à exagérer leurs propres contributions tout en minimisant celles des chercheurs humains dont les travaux ont rendu ces résultats possibles. L’enjeu dépasse la susceptibilité académique : si les décideurs et les bailleurs de fonds prennent ces annonces au pied de la lettre, ils pourraient conclure, à tort, que les mathématiciens humains sont devenus moins nécessaires qu’ils ne le sont réellement.

C’est très exactement le risque que nous signalons régulièrement dans nos Briefings sur l’IA générative en entreprise : une direction générale qui prend une démonstration produit pour une preuve de capacité opérationnelle, et qui en tire des décisions de dimensionnement d’équipe prématurées. La mécanique de l’emballement médiatique fonctionne de la même façon, que le sujet soit un conjecture centenaire ou un cas d’usage Copilot.

Ce que l’on doit en retenir

Trois enseignements concrets se dégagent de cet épisode, transposables sans effort au contexte de l’entreprise.

Premièrement, une preuve formelle n’est pas une preuve d’originalité. Un certificat Lean, comme un audit de sécurité ou une certification de conformité, atteste d’une propriété précise et rien d’autre. Vérifier qu’un raisonnement est logiquement cohérent ne dit rien de ce qu’il doit aux travaux antérieurs, ni de sa portée réelle. La même prudence s’impose face aux benchmarks IA fournis clé en main par les éditeurs : un score élevé sur un test standardisé ne garantit ni l’absence de contamination des données d’entraînement, ni la pertinence du test pour votre cas d’usage métier.

Deuxièmement, le coût affiché en avant-première n’est presque jamais le coût de production réel. Que ce soit 2 000 dollars pour dix théorèmes ou un prix par token pour un agent IA en production, le chiffre marketing capture le meilleur scénario, pas la moyenne opérationnelle observée après itérations, corrections et supervision humaine.

Troisièmement, la vitesse de correction d’un éditeur après contestation publique en dit souvent plus long que sa communication initiale. OpenAI a corrigé sa formulation seulement après que Kun a exprimé son désaccord, et sans note de transparence publique sur ce changement. Face à un partenaire IA, la vraie question de gouvernance n’est pas seulement « que dit le communiqué de lancement », mais « comment réagit l’éditeur lorsqu’un tiers indépendant conteste une affirmation ».

Et la suite ?

Reste une question que les mathématiciens eux-mêmes n’ont pas tranchée : ces résultats ouvrent-ils de nouvelles directions de recherche, ou se contentent-ils de cocher des cases sur une liste de problèmes réputés difficiles ? Maynard se montre prudent sur ce point, estimant que les résultats publiés relèvent davantage de techniques existantes poussées plus loin et combinées avec habileté que d’une idée mathématique véritablement nouvelle, tout en reconnaissant qu’il est encore trop tôt pour trancher définitivement. C’est également la question que devrait se poser tout DSI avant de généraliser un pilote IA à l’ensemble de l’organisation : l’outil résout-il un problème existant plus vite, ou change-t-il la nature des problèmes qu’on peut désormais se poser ? La nuance, ici comme en théorie des groupes, fait toute la différence entre un gain de productivité ponctuel et une transformation durable.

Source très interessante pour aller plus loin dans la reflexion : Robert Hart, « The AI takeover of mathematics has begun », The Verge, août 2026. https://www.theverge.com/ai-artificial-intelligence/977273/the-ai-takeover-of-mathematics-has-begun