Illinois a rassemblé 12 151 problèmes ouverts pour tester si l'IA peut les résoudre

Une équipe de l'Université de l'Illinois à Urbana-Champaign a publié OpenFrontiers : un catalogue de 12 151 problèmes scientifiques ouverts et un test de 200 problèmes mathématiques. Le test pose une question simple : un agent IA sait-il redécouvrir une solution que la science vient tout juste de trouver ? L'agent voit les problèmes tels qu'ils étaient formulés avant leur résolution. La réponse n'est pas jugée par un humain, mais par un programme vérificateur. Le bilan est décevant pour les partisans du « l'IA fait déjà avancer la science » : en mode sans internet, le meilleur résultat est de 7 problèmes résolus sur 40.

Carte du non-résolu : le contenu du catalogue

Jusqu'ici, les problèmes ouverts étaient dispersés entre des listes de conférences, des pages de prix, des blogs et des sections d'articles de synthèse. Chaque source a ses propres règles : comment formuler un énoncé, comment indiquer son statut, sous quelle licence le conserver. Les auteurs ont fusionné 71 sources dans un schéma unique ; 62 d'entre elles ont fourni les textes des problèmes. Les 4 751 autres entrées restent dans le catalogue sous forme d'index, avec uniquement des liens.

Ce que contient le corpus :

• 11 349 entrées (93,4%) relèvent des mathématiques. Viennent ensuite la physique (339), l'informatique (285) et le machine learning (70). • Les problèmes se concentrent surtout en théorie des nombres (2 867) et en géométrie et topologie (2 371). • Principales sources : TheoremDB (3 909), les listes de l'American Institute of Mathematics (3 470), le projet Formal Conjectures (459). • 65,9% des entrées portent un code de la classification MSC 2020, utilisée en mathématiques. • Seules 1 946 entrées, soit 16%, disposent d'une formulation en Lean 4. Lean est un langage dans lequel on écrit une preuve de façon que l'ordinateur en vérifie chaque étape.

Les auteurs n'enjolivent pas le statut des problèmes. Pour 46% des entrées, il est indiqué comme indéterminé : la source ne dit simplement pas si le problème est résolu aujourd'hui. Les doublons n'ont pas été supprimés, pour ne pas réécrire les énoncés des autres.

Comment le test est construit, et pourquoi une « date de coupure » ne suffit pas

OpenFrontiers-Bench se compose de deux parties. Rediscovery-110 regroupe 110 problèmes qui étaient ouverts avant 2026 et dont une solution a été trouvée depuis. Toutes les preuves de ces résolutions sont datées d'après le 5 janvier 2026. Open-90 regroupe 90 problèmes toujours non résolus. Pour 85 des problèmes résolus, il existe une preuve vérifiée en Lean ou un certificat fini exact, par exemple un contre-exemple recalculé en arithmétique exacte.

Chacun des 200 problèmes a une formulation en Lean 4 (version 4.33.1, bibliothèque Mathlib). 93 formulations sont reprises mot pour mot de Formal Conjectures, 47 sont adaptées et 60 sont écrites de zéro. Chaque formulation a été examinée par deux relecteurs : l'un la comparait à l'énoncé d'origine, l'autre essayait d'en briser le sens. Ces deux relecteurs sont des modèles de langage, pas des mathématiciens humains. Aucune remarque critique ne subsiste ; pour 23 problèmes, les deux vérifications n'ont relevé que des remarques mineures.

La construction du test a révélé un point gênant. Pour 55 des 110 solutions, les auteurs des sources attribuent les mathématiques clés à des systèmes d'IA. Si un modèle de la même « lignée » a produit la solution, on ne peut pas parler de redécouverte. Une date de coupure ne suffit donc pas : le protocole exclut ces problèmes pour chaque modèle séparément. Le mode principal est le closed-book, c'est-à-dire un travail sans accès au réseau.

Ce que montrent les sept agents

Les agents ont été testés sur HQ-50 : 50 problèmes sélectionnés pour leur qualité, dont 40 résolus. Trois conditions ont été appliquées : sans internet, avec une copie figée du moteur de recherche et avec le web en direct. Seule comptait une preuve en Lean acceptée par deux programmes vérificateurs indépendants, dans un bac à sable isolé.

• Sans internet, les agents résolvent de 0 à 7 problèmes sur 40. Ce sont surtout trois problèmes que les humains ont résolus par une courte construction. • Avec le web en direct, le meilleur résultat est de 27 problèmes. Presque toujours, l'agent commençait par trouver une solution publiée. • Aucun agent n'a fermé un problème réellement ouvert sans avoir trouvé de solution au préalable. • Les agents performants abandonnent souvent sans avoir épuisé leur budget de temps lorsque le problème est trop difficile.

Ce qu'il faut en retenir

Les mesures de type olympiades et examens, dont la réponse est connue d'avance, ne distinguent plus une vraie recherche d'une bonne recherche documentaire. OpenFrontiers montre comment séparer les deux : interdire le réseau, poser le problème dans sa formulation d'avant la résolution et n'accepter qu'un résultat vérifié formellement. Pour les laboratoires et les investisseurs, c'est un filtre utile face aux déclarations tapageuses sur les « IA scientifiques ». Pour les chercheurs, c'est une carte prête à l'emploi du non-résolu et un ensemble de problèmes dont on ne peut pas attribuer le succès à une fuite des données d'entraînement.

Le dispositif a aussi des limites. Le test est presque entièrement mathématique, et les formulations en Lean n'existent que pour une petite partie du corpus. La vérification des formulations a été faite par des modèles, même si elle s'est déroulée en deux passes indépendantes. Les données et le test sont publiés sur Hugging Face, dans la collection FlippyDora/openfrontiers.