Contexte des annonces
Le lundi, OpenAI a présenté trois résultats majeurs générés par IA : une preuve du conjecture de Kakeya dans toutes les dimensions, une réfutation de l’hypothèse du temps exponentiel en informatique théorique, et une étude du modèle standard centrée sur la chromodynamique quantique et la théorie de Yang‑Mills. Après avoir diffusé des centaines de prépublications en octobre, l’entreprise a introduit des « shepherds » – des experts désignés pour choisir le mode de diffusion de chaque découverte. La sortie du résultat mathématique a consisté en la publication du texte généré, le résultat informatique sera expliqué par un groupe externe, et le résultat physique est actuellement différé en attendant l’avis d’experts.
Méthodologie et vérification
Le conjecture de Kakeya, lié à la façon minimale de faire tourner une aiguille dans toutes les directions, était déjà partiellement résolu en trois dimensions, ce qui a valu le Fields Medal à Hong Wang. OpenAI affirme avoir généré une preuve formelle en Lean, un langage de vérification assistée par ordinateur. Brendan Hassett, professeur à Brown, juge la preuve « bien soutenue », mais souligne qu’il n’a pas encore inspecté le script Lean, indispensable pour valider la logique algorithmique. En informatique, la prétendue réfutation de l’hypothèse du temps exponentiel remet en cause l’idée que certains problèmes exigent un temps de calcul proche du brut‑force, un principe adjacent à la question P vs NP, l’un des sept problèmes du Millénaire. Le résultat physique explore la chromodynamique quantique et son articulation avec la théorie de Yang‑Mills, sans toutefois aborder le problème du « mass gap », également classé parmi les Millénaire. Tous les trois travaux reposent sur des modèles IA capables de générer des démonstrations formelles, mais la publication dépend d’une validation humaine et d’une formalisation complète dans Lean.
Réactions de la communauté scientifique
Les chercheurs interrogés par The Verge expriment une fatigue croissante face à la stratégie de diffusion sélective. Constantin Kogler (Institute for Advanced Study) accepte la réduction du volume de prépublications, mais critique le fait que seuls des scientifiques choisis puissent examiner les preuves. Andreas Karch (University of Texas) qualifie la sélection d’« désastre », rappelant le pouvoir déjà important des grands laboratoires. L’Advisory Group on Mathematics and Artificial Intelligence (AGMAI) a publié une mise en garde la veille, recommandant la mise à disposition immédiate des sorties en langage naturel et Lean sur des dépôts ouverts, ainsi que le financement de la communauté pour l’analyse. L’absence de ces mesures, selon AGMAI, crée un risque de biais de sélection et de retard dans la validation.
Implications et limites
Si les preuves tiennent, elles pourraient accélérer la résolution de problèmes fondamentaux en mathématiques et en informatique, en montrant que les modèles de langage peuvent produire des arguments vérifiables. Toutefois, la dépendance à un outil de formalisation comme Lean impose une barrière technique : chaque chercheur doit maîtriser ce langage pour reproduire la vérification. Le choix de restreindre l’accès complique la reproduction indépendante, augmente le coût de la validation et peut freiner l’adoption de ces méthodes dans la communauté. Une diffusion ouverte, comme préconisée par AGMAI, permettrait d’évaluer la robustesse des algorithmes IA, de détecter d’éventuelles erreurs de raisonnement et de garantir que les avancées ne restent pas confinées à un cercle restreint.
