OpenAI publie 700 preuves mathématiques et crispe les chercheurs

OpenAI a publié mardi plus de 700 fichiers présentant des preuves pour divers problèmes de mathématiques, quelques jours après la polémique autour de son IA sur les équations de Navier-Stokes. Le groupe de chercheurs qui suit ces sujets y voit moins une avancée scientifique qu’un bras de levier sur la communauté. Le point sensible tient à la méthode : des preuves peuvent être correctes sur le plan formel, mais rester presque illisibles pour des humains.

Une publication massive qui passe mal chez les mathématiciens

La critique est venue d’un groupe appelé Association for Human Mathematics, dont la prise de position a ensuite été relayée par Terence Tao, médaille Fields et figure très écoutée dans le domaine. Dans sa déclaration, le collectif écrit : “Mathematicians have a particular vision of progress that is informed by history and field-specific considerations,” puis ajoute : “We reject OpenAI’s assertion that this release advances our subject, and we urge mathematicians and the public to view the value of this publication model with due skepticism.”

Le ton se durcit encore avec cette formule : “Releasing over 700 files at once is not a demonstration of scholarship, but a demonstration of power.” Le reproche est clair : publier en bloc déplace le coût de la vérification vers les chercheurs, alors même que ces fichiers sont supposés ouvrir de nouvelles pistes.

Lean valide la forme, pas toujours l’usage

OpenAI explique que ses preuves ont été vérifiées avec Lean, un langage de preuve formel utilisé pour vérifier la logique d’une démonstration étape par étape. Sur le papier, cela donne une garantie technique. Dans les faits, la valeur scientifique reste plus floue si les résultats ne peuvent pas être relus facilement par des mathématiciens, ce qui fait tout de même un petit détail quand on parle de démonstration.

Le sujet n’est pas seulement celui de la validité formelle. Il touche aussi à la circulation de la recherche. Quand une entreprise privée publie des résultats issus de modèles inaccessibles à la communauté, elle impose un déséquilibre : la machine produit, les humains décortiquent. Et ce découpage ne plaît pas à tout le monde.

Le groupe consultatif contestait déjà la méthode

OpenAI dit s’appuyer sur un organe externe, Advisory Group on Mathematics and Artificial Intelligence. Mais la note rendue publique à la fin du mois précédent allait dans l’autre sens : “We want to state clearly from the start: we do not endorse this practice, and we ask them to stop testing advanced mathematical problems on proprietary models,” écrivait le groupe.

Cette divergence compte, car elle fragilise l’argument d’autorité mis en avant par OpenAI. L’Association for Human Mathematics accuse ainsi l’entreprise de s’adosser à un groupe d’experts tout en ignorant le cœur de son désaccord. Autrement dit, la consultation existe, mais elle ne débouche pas sur un consensus. Et, dans un domaine aussi normé que les mathématiques, le vernis de légitimité ne suffit pas.

Ce que cette affaire dit du marché de l’IA scientifique

Au-delà de la querelle de méthode, l’épisode montre comment les grands acteurs de l’IA cherchent à s’imposer dans la recherche fondamentale. Publier vite, publier beaucoup, publier sous forme de preuves formelles : la logique est industrielle, presque logistique. Reste à savoir si elle sert vraiment la compréhension scientifique, ou seulement la démonstration de capacité.

Pour les chercheurs, le risque est double. D’un côté, ils doivent vérifier des résultats souvent peu lisibles. De l’autre, ils voient leur travail absorbé dans des systèmes propriétaires qui ne leur donnent ni accès complet, ni contrôle sur le cadre de production. La suite dépendra moins du nombre de fichiers diffusés que de leur capacité à être compris, réutilisés et discutés dans de bonnes conditions.